Translating a State Transition System to properties LTL formulae

Question

In the context of bounded model checking, one describes the system as a State Transition System and the properties that need to be checked. When one needs to provide multiple system descriptions and properties to the Model Checker Tool, it can become tedious to write the property by hand. In my case, I use some temporal logic. How does one automate the process of translating/parsing the system description and deriving verifiable properties from it (ideally, a set of Initial states, Transitions, Set of States). For example, consider the Microwave Example given here Given such a system description, how can I arrive at the specifications in an efficient manner? There is no such open source tool that I know of, that can do this. Any approaches in terms of ideas, theories are welcome.

Answer 1

You can't automatically derive LTL formulae from automata as you suggest, because automata are more expressive than LTL formulae.

That leaves you with mainly two options: 1. find a verification tool which accepts specifications that are directly expressed as automata (I'm not sure which ones do, but I suspect it is worth checking SPIN and NuSMV for this feature.), or 2. use a meta-specification language that makes the writing of specifications easier; for example, https://www.isp.uni-luebeck.de/salt (doi: 10.1007/11901433_41) or IEE1850/PSL. While PSL is more a language definition for tool-implementors, SALT already offers a web front-end that translates your input straight into LTL.

(By the way, I find your approach methodologically challenging though: you're not supposed to derive formulae from your model, but from your initial system description as it is this very model which you're going to verify. But I am not a 100% sure, if I understood this point in your question correctly.)

Answer 2

I think properties of a system, e.g. Microwave system, come from technical and common sense expectation and requirements, not the model. E.g. microwave is supposed to cook the food. But it is not supposed to cook with door open. Nevertheless a repository of typical LTL pattern can be useful to define properties. It also lists properties along with more familiar regex and automata properties.

If you certain you still want to translate automata to LTL automatically check https://mathoverflow.net/questions/96963/translate-a-buchi-automaton-to-ltl

Kansas Specification Property Repository http://patterns.projects.cs.ksu.edu/documentation/patterns.shtml