MightyPPL

This is a tool for translating MITPPL formulae over timed words into timed automata in

• Uppaal xml format.
• TChecker model format.

The most common applications are satisfiability and model checking: these TAs can be analysed by Uppaal (for the finite-word case; see also pyuppaal, pyUPPAAL), (multi-core) LTSmin (for the infinite-word case), or TChecker.

MITPPL is a very expressive timed logic that contains the full fragment of MITL (with both future and past modalities) and Pnueli modalities of the form $\mathbf{P \mkern -2mu n}_{[0, u \rangle}(\phi_1, \dots, \phi_n)$ (and their duals and past counterparts). Please note that MightyPPL adopts the strict-future semantics for all temporal modalities---the weak-future "until" $\mathbf{U}^\textit{w}_I$ can be emulated by, for example when $0 \in I$, $\varphi_1 \mathbf{U}^\textit{w}_I \varphi_2 \iff \varphi_2 \lor \big(\varphi_1 \land (\varphi_1 \mathbf{U}_I \varphi_2)\big)$.

Below are some example formulae supported by MightyPPL (all unsatisfiable over infinite timed words):

(p1 U[1, 2] p2) && G[1, 3] (!p2)

This is unsatisfiable, as you cannot have a $p _2$-event in $t + [1, 2]$ and simultaneously have no $p _2$-event in $t + [1, 3]$. It becomes satisfiable if the intervals are swapped.

Fn[0, 5](p1, p2, p3) && G(p1 -> G[0, 3](!p2)) && G(p2 -> G[0, 3](!p3))

Clearly unsatisfiable. If the interval is $[0, 7]$ then satisfiable.

F( !((p1 -> (p1 && H [0, 20] p1)) || O [0, 30] (p1 -> (p1 && H [0, 20] p1))) )

The formula holds if there is a point where $p _1 \land \textbf{O} _{[0, 20]} (\neg p _1)$ and $\textbf{H} _{[0, 30]} \big( p _1 \land \textbf{O} _{[0, 20]} (\neg p _1) \big)$ both hold. This is impossible as $\textbf{O} _{[0, 20]} (\neg p _1)$ and $\textbf{H} _{[0, 30]} p _1$ are contradictory. It becomes satisfiable if $[0, 20]$ and $[0, 30]$ are swapped.

See some additional sanity checks below.

Formula	Sat?
$\mathbf{F} \big((p \mathbf{S} _{[1,2]} q) \land \neg (p \mathbf{S} _{[1,3]} q)\big)$	✗
$\mathbf{F} \big((p \mathbf{S} _{[1,3]} q) \land \neg (p \mathbf{S} _{[1,2]} q)\big)$	✓
$\mathbf{F} \big((p \mathbf{U} _{[1,2]} q) \land \neg (p \mathbf{U} _{[1,3]} q)\big)$	✗
$\mathbf{F} \big((p \mathbf{U} _{[1,3]} q) \land \neg (p \mathbf{U} _{[1,2]} q)\big)$	✓
$\mathbf{F} \big((p \mathbf{U} _{[1,2]} q) \land \neg (p \mathbf{U} _{[0,3]} q)\big)$	✗
$\mathbf{F} \big((p \mathbf{U} _{[0,3]} q) \land \neg (p \mathbf{U} _{[1,2]} q)\big)$	✓

See the grammar file Mitl.g4 for the exact syntax of input formulae, but in short: F, G, U, R as in MightyL,

• O (once) is the past version of F,
• H (historically) is the past version of G,
• S (since) is the past version of U, and
• T (trigger) is the past version of R.

Pnueli modalities (and their past and dual versions) are Fn, On, Gn and Hn.

Usage

mitppl <in_spec_file> --{fin|inf} [out_file --{tck|xml} [--{noflatten|compflatten}]] [--debug] [--noback]

• in_spec_file is a formula, written in plain text as the examples above.
• --fin or --inf for finite / infinite timed words (finite / Büchi acceptance).
• If out_file is specified then either --tck or --xml must follow.
• Operation modes:
  • The "noflatten" mode: individual tester / component TAs, one or more for each temporal subformula;
  • The "compflatten" mode (recommended): individual tester TAs, one for each temporal subformula;
  • The default "flatten" mode: a single monolithic TA for the entire formula (the synchronous product of the tester and component TAs). For performance reasons MightyPPL constructs only forward-reachable state spaces and transitions.
• If out_file is unspecifed, then an implementation of the standard backward fixpoint algorithm will be used as the back end.
• --debug to pause at various points in the processing.
• --noback to disable the backward reachability analysis for simplifying tester TAs (no effect with --noflat).

Currently there are two ways to specify the model $M$ in model checking: edit the generated xml / tck file, or hard-code in MightyPPL.cpp. See the model-checking benchmarks to see how this is done.

Technical details

Internally MightyPPL uses TA and DBM representations provided by MoniTAal and PARDIBAAL. In particular, TAs are represented semi-symbolically and transitions are synchronised on Boolean formulae over propositions (instead of single letters). Without using two-way or other TA variants, future and past modalities are handled uniformly by good old pure vanilla TAs, thanks to the innocuous fact that timed regular languages are closed under reversal (!). Overlapping obligations from MITL modalities with general intervals and Pnueli modalities are handled by a novel sequentialisation technique; see the tech report for details.

Build MightyPPL

Boost >= 1.40 is needed by MoniTAal.

$ git clone git@github.com:hsimho/MightyPPL.git
$ cd MightyPPL

Edit CMakeLists.txt and modify set(ANTLR_EXECUTABLE ...) to point to ANTLR's .jar file (complete Java binaries jar). Then

$ git submodule init
$ git submodule update --force --remote

to check out BuDDy. If these do not work, try

git submodule add -f https://github.com/SSoelvsten/buddy external/buddy
mkdir external/monitaal

beforehand. Finally,

$ mkdir build ; cd build
$ cmake ..
$ make

For the issue with CMake minimum version, edit the following files, modify cmake_minimum_required(VERSION ...) to at least 3.5, and make again.

build/antlr4_runtime/src/antlr4_runtime/runtime/Cpp/_deps/googletest-src/CMakeLists.txt
build/antlr4_runtime/src/antlr4_runtime/runtime/Cpp/_deps/googletest-src/googlemock/CMakeLists.txt
build/antlr4_runtime/src/antlr4_runtime/runtime/Cpp/_deps/googletest-src/googletest/CMakeLists.txt

Some empirical results

The table below presents the runtime (in seconds) for checking satisfiability over infinite timed words. All experiments were executed on a desktop machine with an Intel i9-13900K CPU and 64GB of memory.
Note in particular that we used identical back ends for all comparisons!
MightyPPL is used in the "compflatten" mode.

Benchmarks in /testcases/MightyL/.

Formula	Sat?	MightyL + opaal_ltsmin	MightyPPL + opaal_ltsmin
E-5-12	✓	225.575	0.461
A-5-12	✓	3.460	0.385
U-5-12	✓	171.445	15.242
R-5-12	✓	2.249	0.424
theta3-100-1000	✓	ERR	0.858
theta4-100-1000	✓	ERR	10.595

Benchmarks in /testcases/newhoxha2/.

Formula	Sat?	MightyL + opaal_ltsmin	MightyPPL + opaal_ltsmin
1	✓	44.444	1.045
2	✗	62.400	7.907
3	✓	-	0.568
4	✗	-	3.752
5	✓	-	0.554
6	✗	-	220.276

Benchmarks in /testcases/acacia/.

Formula	Sat?	MightyPPL + TChecker
3	✓	4.441
4	✗	0.958
5	✓	1.309
6	✗	0.945
9	✓	6.968

Cite MightyPPL

@article{hkmmp2025b,
  author    = {Ho, Hsi-Ming and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Pandya, Paritosh},
  title     = {MightyPPL: Verification of MITL with Past and Pnueli Modalities},
  journal   = {CoRR},
  volume    = {abs/2510.01490},
  year      = {2025},
  url       = {https://arxiv.org/abs/2510.01490},
  archivePrefix = {arXiv},
  eprint    = {2510.01490},
}

License

LGPL-3.0. The MIT License applies to CMake scripts from "Getting started with ANTLR in C++".