6
$\begingroup$

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?

$\endgroup$
  • 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 Clarke Apr 18 '11 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$ – Camilo Apr 18 '11 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 Clarke Apr 18 '11 at 16:11
5
$\begingroup$

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.

  1. 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

  2. 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

  3. 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

$\endgroup$
  • $\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$ – Camilo Apr 21 '11 at 1:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.