# 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:- POTL formula and an Operator Precedence Automata (OPA)
- 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.