Normally model checking with specifications written in CTL*/CTL is done over Kripke structures, however there are ways of doing it over somehow simpler Labelled Transition Systems, for instance ACTL. Does anyone has any pointer on similar logics/techniques?
$\begingroup$
$\endgroup$
3
-
1$\begingroup$ It would be easier to answer this question if we knew a bit more about what you already know. Do you know Hennessy-Milner logic? What about the modal $\mu$-calculus? Or ACTL* (oai.cwi.nl/oai/asset/1624/1624A.pdf)? $\endgroup$– Dave ClarkeCommented Apr 18, 2011 at 6:59
-
$\begingroup$ Dave, I have some notions of μ-calculus and HML, but not any real deep knowledge (which I will have to acquire anyway). For now I'm just looking for reference on time logics applied over LTSs as a starting point. $\endgroup$– CamiloCommented Apr 18, 2011 at 14:11
-
1$\begingroup$ See entry: cstheory.stackexchange.com/questions/4952/…, whose answers should provide you with what you need, including tools working with LTSs such as mCRL and mCRL too. $\endgroup$– Dave ClarkeCommented Apr 18, 2011 at 16:11
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
The meaning of simpler in your question is unclear. Kripke structures have a labelling function on states. LTSes have labels on transitions, which can be viewed as a labelling function on transitions. Why is one simpler than the other? In the context of your question, using acronyms like "ACTL" is ambiguous because the "A" could mean all paths or action-based.
The difference, in my opinion, between Kripke structures and LTSes is based on modelling convenience and not simplicity. There is a lot of work comparing and contrasting the two. Here are a few starting points for chasing down related work.
De Nicola and Vaandrager have a few papers on translating between Kripke structures and LTSes and how this affects logical properties. They introduce doubly labelled transition systems to move between the two types of representations and semantic interpretations.
Action versus state based logics for transition systems , De Nicola and Vaandrager, 1990
Three logics for branching bisimulation, De Nicola and Vaandrager, 1995
If the goal is verification of event-based systems, one option is to translate the LTS into a Kripke structure and use a Kripke structure model checker. The translation has to preserve the interpretation of CTL over the LTS.
An action-based framework for veryfying logical and behavioural properties of concurrent systems, De Nicola, Fantesi, Gnesi, Ristori
Translating between representations involves a blowup. For the case of LTL, there are cases when this blowup can be avoided. Here is a recent paper on the topic.
State/event-based software model checking, Chaki, Clarke, Ouaknine, Sharygina, Sinha
-
$\begingroup$ Thanks, and yes simpler is probably a bad adjective to attach, maybe I used it because I learned LTSs first so they seem more natural to me but objectively there is no reason why they are simpler. Thanks for the links they do seem to be what I'm looking for. $\endgroup$– CamiloCommented Apr 21, 2011 at 1:57