<p>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. </p>

<p>The <a href="http://spinroot.com/spin/whatispin.html">SPIN model checker</a> is a widely-used tool for model-checking LTL properties. </p>

CC BY-SA 2.5
2011-02-16T12:25:37.817Z
2011-02-16T12:25:37.817Z
Neel Krishnaswami
<p>Another two tools, to complement the one suggested by Neel, are <a href="http://homepages.cwi.nl/~mcrl/mutool.html">muCRL</a> and <a href="http://www.mcrl2.org/mcrl2/wiki/index.php/Home">mCRL2</a>. 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 <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.143.9834&amp;rep=rep1&amp;type=pdf">propositional modal mu calculus</a>, 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. </p>

CC BY-SA 2.5
2011-02-16T13:22:00.717Z
I didn't know the modal mu-calculus was decidable! Now I'm off to look at the proof in your link...
Neel Krishnaswami
CC BY-SA 2.5
2011-02-16T15:18:04.393Z
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
CC BY-SA 2.5
2011-02-16T12:47:01.903Z
2011-02-16T15:20:06.390Z
2011-02-16T15:20:06.390Z
Dave Clarke
<p>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: <a href="http://pub.ist.ac.at/gametheory/" rel="nofollow">http://pub.ist.ac.at/gametheory/</a> 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).</p>

CC BY-SA 2.5
2011-02-17T20:27:01.127Z
The model checking problem is in $NP\cap coNP$. The decision problem is $EXP$-time complete, I believe.
Mark Reitblatt
CC BY-SA 4.0
2020-10-12T18:38:45.223Z
@MarkReitblatt I'm a bit confused now.  Wikipedia says that model checking linear modal mu calculus is PSPACE-complete, and I was under the impression that linear modal mu calculus is a proper subset of modal mu calculus and thus model checking modal mu calc should also be PSPACE-complete.  In which step did I go awry here?
wanderingmathematician
CC BY-SA 3.0
2011-02-17T19:45:25.710Z
2011-04-18T16:12:55.247Z
2011-04-18T16:12:55.247Z
Aubrey da Cunha
<p>CTL properties can be checked in linear time (see <a href="http://scholar.google.co.uk/scholar?cluster=326651136244218780" rel="nofollow">Clarke et al</a>).</p>

<p>Long time ago I used to work in a company where many colleagues used <a href="http://www.research.ibm.com/haifa/projects/verification/RB_Homepage/" rel="nofollow">Rulebase</a> to verify integrated circuit designs. The property language is <a href="http://dx.doi.org/10.1109/IEEESTD.2005.97780" rel="nofollow">PSL</a>, it is standardized by IEEE, and is a kind of CTL on steroids.</p>

CC BY-SA 3.0
2011-04-19T09:49:54.247Z
I doubt FRELIMO was modelchecked with CTL - you may wish to correct that link.
reinierpost
CC BY-SA 3.0
2011-04-19T12:10:30.180Z
Fixed. Maybe Google Scholar changed their IDs? I don't remember seeing "FRELIMO" ever before.
Radu GRIGore
CC BY-SA 3.0
2011-02-17T14:43:53.090Z
2011-04-19T12:09:25.530Z
2011-04-19T12:09:25.530Z
Radu GRIGore
<p>In a course I got to know <a href="http://www.cl.cam.ac.uk/research/hvg/Isabelle/" rel="nofollow">Isabelle</a>, 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.</p>

CC BY-SA 2.5
2011-02-17T15:39:55.073Z
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
CC BY-SA 2.5
2011-02-17T17:18:52.080Z
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
CC BY-SA 3.0
2013-03-04T16:49:19.980Z
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
CC BY-SA 2.5
2011-02-17T09:54:53.057Z
2011-02-17T09:54:53.057Z
Raphael
<p>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.</p>

<p>Back in 1990, R. De Nicola and F. Vaandrager introduced ACTL as an action-based CTL (<em>Action versus state based logics for transition systems</em>, 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: <em>An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems</em>, Computer Networks and ISDN Systems, Vol. 25, No. 7., pp. 761-778.) and more recently in 2008 (R. Meolic, T. Kapus, Z. Brezočnik: <em>ACTLW - An Action-based Computation Tree Logic With Unless Operator</em>, Information Sciences, 178 (6), pp. 1542-1557.)</p>

<p>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.</p>

CC BY-SA 3.0
2011-10-26T20:48:58.183Z
2013-05-24T07:47:43.613Z
2013-05-24T07:47:43.613Z
meolic
<p>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.</p>

CC BY-SA 2.5
2011-02-16T11:58:06.343Z
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
CC BY-SA 2.5
2011-02-16T12:08:47.720Z
@Dave Clarke edited
Gabriel Ščerbák
CC BY-SA 2.5
2011-02-17T00:21:39.420Z
The second result on Googling "Labelled Transition Systems": http://www.doc.ic.ac.uk/ltsa/
Kaveh
CC BY-SA 2.5
2011-02-17T02:29:54.253Z
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
<lo.logic><formal-modeling><model-checking><program-verification><automated-theorem-proving>
What are practically computable properties of Labelled Transition Systems?
Gabriel Ščerbák
# What are practically computable properties of Labelled Transition Systems?

(Asked by: username_0 on 2011-02-16)

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.

**Tags:** lo.logic, formal-modeling, model-checking, program-verification, automated-theorem-proving

> **Comments:**
> **username_1**: 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?  
> **username_0**: @username_1 edited  
> **username_2**: The second result on Googling "Labelled Transition Systems": http://www.doc.ic.ac.uk/ltsa/  
> **username_0**: 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.  

---

## 6 answers

### Answer by username_3 on 2011-02-16. Score: 11

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](http://spinroot.com/spin/whatispin.html) is a widely-used tool for model-checking LTL properties.


---

### Answer by username_1 on 2011-02-16. Score: 11

Another two tools, to complement the one suggested by Neel, are [muCRL](http://homepages.cwi.nl/~mcrl/mutool.html) and [mCRL2](http://www.mcrl2.org/mcrl2/wiki/index.php/Home). 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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.143.9834&rep=rep1&type=pdf), 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.

> **Comments:**
> **username_3**: I didn't know the modal mu-calculus was decidable! Now I'm off to look at the proof in your link...  
> **username_4**: 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.  

---

### Answer by username_5 on 2011-02-17. Score: 5

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

> **Comments:**
> **username_4**: The model checking problem is in $NP\cap coNP$. The decision problem is $EXP$-time complete, I believe.  
> **username_6**: @MarkReitblatt I'm a bit confused now.  Wikipedia says that model checking linear modal mu calculus is PSPACE-complete, and I was under the impression that linear modal mu calculus is a proper subset of modal mu calculus and thus model checking modal mu calc should also be PSPACE-complete.  In which step did I go awry here?  

---

### Answer by username_7 on 2011-02-17. Score: 3

CTL properties can be checked in linear time (see [Clarke et al](http://scholar.google.co.uk/scholar?cluster=326651136244218780)).

Long time ago I used to work in a company where many colleagues used [Rulebase](http://www.research.ibm.com/haifa/projects/verification/RB_Homepage/) to verify integrated circuit designs. The property language is [PSL](http://dx.doi.org/10.1109/IEEESTD.2005.97780), it is standardized by IEEE, and is a kind of CTL on steroids.

> **Comments:**
> **username_8**: I doubt FRELIMO was modelchecked with CTL - you may wish to correct that link.  
> **username_7**: Fixed. Maybe Google Scholar changed their IDs? I don't remember seeing "FRELIMO" ever before.  

---

### Answer by username_9 on 2011-02-17. Score: 2

In a course I got to know [Isabelle](http://www.cl.cam.ac.uk/research/hvg/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.

> **Comments:**
> **username_9**: 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?  
> **username_9**: 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.  
> **username_10**: 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.  

---

### Answer by username_11 on 2011-10-26. Score: 2

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.


---

