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.
$\begingroup$
$\endgroup$
4
-
1$\begingroup$ 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? $\endgroup$– Dave ClarkeCommented Feb 16, 2011 at 11:58
-
$\begingroup$ @Dave Clarke edited $\endgroup$– Gabriel ŠčerbákCommented Feb 16, 2011 at 12:08
-
2$\begingroup$ The second result on Googling "Labelled Transition Systems": doc.ic.ac.uk/ltsa $\endgroup$– KavehCommented Feb 17, 2011 at 0:21
-
$\begingroup$ 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. $\endgroup$– Gabriel ŠčerbákCommented Feb 17, 2011 at 2:29
Add a comment
|
6 Answers
$\begingroup$
$\endgroup$
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.
answered Feb 16, 2011 at 12:25
$\begingroup$
$\endgroup$
2
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.
answered Feb 16, 2011 at 12:47
-
$\begingroup$ I didn't know the modal mu-calculus was decidable! Now I'm off to look at the proof in your link... $\endgroup$ Commented Feb 16, 2011 at 13:22
-
5$\begingroup$ 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. $\endgroup$ Commented Feb 16, 2011 at 15:18
$\begingroup$
$\endgroup$
2
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).
-
3$\begingroup$ The model checking problem is in $NP\cap coNP$. The decision problem is $EXP$-time complete, I believe. $\endgroup$ Commented Feb 17, 2011 at 20:27
-
$\begingroup$ @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? $\endgroup$ Commented Oct 12, 2020 at 18:38
$\begingroup$
$\endgroup$
2
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.
-
$\begingroup$ I doubt FRELIMO was modelchecked with CTL - you may wish to correct that link. $\endgroup$ Commented Apr 19, 2011 at 9:49
-
$\begingroup$ Fixed. Maybe Google Scholar changed their IDs? I don't remember seeing "FRELIMO" ever before. $\endgroup$ Commented Apr 19, 2011 at 12:10
$\begingroup$
$\endgroup$
3
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.
-
1$\begingroup$ 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? $\endgroup$– RaphaelCommented Feb 17, 2011 at 15:39
-
1$\begingroup$ 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. $\endgroup$– RaphaelCommented Feb 17, 2011 at 17:18
-
$\begingroup$ 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. $\endgroup$– MakariusCommented Mar 4, 2013 at 16:49
$\begingroup$
$\endgroup$
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.
