PV2 ⊧ Cervinotransforms first order LTL formulae to Electrum models

Tool to translate a typical First-Order Linear Temporal Logic (FOLTL) specification into two of its decidable fragments.

Application domain/field

• First-Order Linear Temporal Logic (FOLTL)
• Specification transformation/translation

Type of tool

Specification translator?

Expected input

• Cervino specification
• Property to be checked

Format:

Cervino file

Expected output

If the process is automated with the -s option, then it will report either SAT or UNSAT. Otherwise, it generates a file output.als which can be analyzed with the Electrum Analyzer.

Internals

The tool takes a Cervino specification as input and generates Electrum models which are given to the Electrum Analyzer, which calls a complete procedure in nuXmv.

Comments

Cervino seems to be both a name for the modelling language and for the tool.