PV3 ⊧ POMCchecks whether a user-specified POTL formula holds for an automaton or MiniProc program

Model checker for POTL temporal logic This temporal logic can express context-free properties.

Application domain/field

• Model checking
• Explicit-state model checking
• Context-free properties
• Temporal logic
• POTL (Precedence-Oriented Temporal Logic)
• Procedural programs

Type of tool

Model checker

Expected input

One of the following two:

1. POTL formula and an Operator Precedence Automata (OPA)
2. POTL formula and a MiniProc program

Format:

.pomc file (own format, it contains the POTL formula and the automaton/MiniProc program)

Expected output

True or False indicating whether the OPA/MiniProc program satisfy the formula. If a formula is rejected, then a (partial) counterexample trace is also provided.

Internals

Given a POTL formula, it builds an automaton equivalent to this formula. Then it checks whether the intersection between this automaton and the input model is empty. POTL (Precedence-Oriented Temporal Logic) is strictly more expressive than LTL.