Formula Generation

This page explains how to generate propositional formulas with linear arithmetic from Timed Constraint Automata. For detailed explanations of the formulas, please see the reference at the bottom of the page.

The intended use of these formulas is within a framework for bounded model checking of Timed Constraint Automata. For more information about propositional formulas in bounded model checking, please see the references at the bottom of the page.

The formula generation is invoked from the TCA editor as shown below:

The wizard which opens presents several options, most of which may be left at their default values. The first page

allows to choose the unfolding depth (for bounded model checking), the range of data values, and the output file (project) name. The second page

allows to choose the TCA for which to generate the code. If the file contains more than one automaton, formulas are generated for the product of all selected automata. The third page

allows to choose up to one location per automaton, to generate a simple reachability property for. More complex properties need to be specified manually in the generated .msat file.

The plugin only supports generation of formulas for the MathSAT4 solver. As soon as more formula formats are supported, a corresponding option will be available.

References

Stephanie Kemper.
Proceedings of the 8th International Workshop on the Foundations of Coordination Languages and Software Architectures, FOCLASA'09,
Electronic Notes in Theoretical Computer Science, Volume 255, 2009

Edmund M. Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu.
Formal Methods in System Design, Volume 19, Issue 1, Pages 7–34, 2001.