What are practically computable properties of Labelled Transition Systems?

I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would like to re-use existing solutions to see if they are useful for my appication. I would like to know what properties of LTSs (and use cases) can be easily automatically proved, so I can decide, if there is a practical counterpart to the problem for use cases.

• you need to be more precise. What do you want to prove? Do you want an automatic tool for proving the properties? What is your application? – Dave Clarke Feb 16 '11 at 11:58
• @Dave Clarke edited – Gabriel Ščerbák Feb 16 '11 at 12:08
• The second result on Googling "Labelled Transition Systems": doc.ic.ac.uk/ltsa – Kaveh Feb 17 '11 at 0:21
• Thank you all very much for your help, I haven't awaited these much help. Now I have much to read and until I am done, I cannot fairly accept any answer, unless some stands out by votes. So please be patient. – Gabriel Ščerbák Feb 17 '11 at 2:29

The formulas of Hennessy-Milner logic are very easy to prove about labelled transition systems. However, this logic is inexpressive enough (there is no way to state properties of infinite paths) that you will probably wish to consider some extension to it, such as linear temporal logic. LTL has a decidable, but PSPACE-complete, problem.

The SPIN model checker is a widely-used tool for model-checking LTL properties.

Another two tools, to complement the one suggested by Neel, are muCRL and mCRL2. Both toolsets have quite a range of tools for defining LTS at various levels of abstraction. State space visualisation and model checking tools are also available. The underlying logic is the propositional modal mu calculus, which is much more expressive than LTL, yet still decidable. Other useful tools allow you to perform state space reduction modulo bisimulation to get the smallest representation of your system.

• I didn't know the modal mu-calculus was decidable! Now I'm off to look at the proof in your link... – Neel Krishnaswami Feb 16 '11 at 13:22
• Propositional modal $\mu$-calculus is decidable; I believe Street and Emerson showed this in the 80's. First-order certainly is not: it's complete for the first level of the analytic hierarchy, if I recall. BTW, I absolutely love that survey by Bradfield and Stirling. I think it's one of the best written accounts of the theory of $\mu$-calculus. – Mark Reitblatt Feb 16 '11 at 15:18

To expand on Dave's answer, the modal mu calculus is also tied to the notion of infinite parity games. There is a very good set of lecture notes available here: http://pub.ist.ac.at/gametheory/ that present the connection. As a side note, not only is the modal mu-calculus decidable, it's in $\mathit{NP}\cap \mathit{co\text{-}NP}$ (see lecture notes).

• The model checking problem is in $NP\cap coNP$. The decision problem is $EXP$-time complete, I believe. – Mark Reitblatt Feb 17 '11 at 20:27

CTL properties can be checked in linear time (see Clarke et al).

Long time ago I used to work in a company where many colleagues used Rulebase to verify integrated circuit designs. The property language is PSL, it is standardized by IEEE, and is a kind of CTL on steroids.

• I doubt FRELIMO was modelchecked with CTL - you may wish to correct that link. – reinierpost Apr 19 '11 at 9:49
• Fixed. Maybe Google Scholar changed their IDs? I don't remember seeing "FRELIMO" ever before. – Radu GRIGore Apr 19 '11 at 12:10

In a course I got to know Isabelle, a "generic proof assisstant". It supports (total) functional programming (close to ML) and higher order logic. You can define yourself (or find) languages for LTS and LTL and prove theorems on those. I do not know if this qualifies as easy, but it certainly works.

• I read (one part of) the question as "What are tools that help me prove properties of LTS?", and prove assisstants came to mind. You are certainly right, others might do the job as well, but I can't very well claim they do if I don't know that for sure, can I? – Raphael Feb 17 '11 at 15:39
• Radu, I interpolated. Note that tools such as Isabelle have the capability to automate proofs, although they might be weaker in a specific application (since they are general tools). They might be more helpful than specialised tools if you want to prove properties those tools can not automatically prove. – Raphael Feb 17 '11 at 17:18
• It is interesting to see how the term "generic proof assistant" that L. Paulson introduced in 1989 can be interpreted these days. This is perfectly OK. Originally, the idea was to have a generic logical framework for fumulating the Martin-Löf Type Theory of the week (which was changing a lot at that time). Later the framework was re-used for Isabelle/ZF, again later for Isabelle/HOL, which is now the main application. – Makarius Mar 4 '13 at 16:49

If your background is CTL interpreted over Kripke structures and you looks for something similar interpreted over LTSs, than ACTL (action-based CTL) could be interesting.

Back in 1990, R. De Nicola and F. Vaandrager introduced ACTL as an action-based CTL (Action versus state based logics for transition systems, Semantics of Systems of Concurrent Processes (1990), pp. 407-419). It has been further studied in 1993 (R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori: An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems, Computer Networks and ISDN Systems, Vol. 25, No. 7., pp. 761-778.) and more recently in 2008 (R. Meolic, T. Kapus, Z. Brezočnik: ACTLW - An Action-based Computation Tree Logic With Unless Operator, Information Sciences, 178 (6), pp. 1542-1557.)

Main idea of ACTL (not to be confused with a subset of CTL with the same acronym) is to have similar operators and similar algorithms for model checking as those for CTL. Moreover, operators are defined by fixed-point expressions analog to those used for CTL. The complexity (I am not sure about expresiveness) of ACTL is somewhere between HML and propositional modal μ-calculus.