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

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.
Automaton Model checking

Links

Related papers

Model-Checking Structured Context-Free Languages (CAV '21)

Last publication date

15 July 2021

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.