PV3 ⊧ POMCchecks whether a user-specified POTL formula holds for an automaton or MiniProc programModel checker for POTL temporal logic This temporal logic can express context-free properties.
- Model checking
- Explicit-state model checking
- Context-free properties
- Temporal logic
- POTL (Precedence-Oriented Temporal Logic)
- Procedural programs
Type of toolModel checker
Expected inputOne of the following two:
- POTL formula and an Operator Precedence Automata (OPA)
- POTL formula and a MiniProc program
.pomc file (own format, it contains the POTL formula and the automaton/MiniProc program)
False indicating whether the OPA/MiniProc program satisfy the formula.
If a formula is rejected, then a (partial) counterexample trace is also provided.