5 papers
Efficient Monitoring of Timed Properties
Thomas Møller Grosen, Thomas Møller Grosen, Sean Kauffman +2
In this paper we study monitoring of real-time systems with respect to properties given by a pair of Timed Büchi Automata, one for the property and one for its complement. This inc…
History-deterministic Parikh Automata
Enzo Erlich, Mario Grobler, Shibashis Guha +3
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable…
On the Existence of Reactive Strategies Resilient to Delay
Martin Fränzle, Paul Kröger, Sarah Winter +1
We compare games under delayed control and delay games, two types of infinite games modelling asynchronicity in reactive synthesis. In games under delayed control both players suff…
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL is Even Harder
Marie Fortin, Louwe B. Kuijer, Patrick Totzke +1
Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are H…
Robust Probabilistic Temporal Logics
Martin Zimmermann
We robustify PCTL and PCTL*, the most important specification languages for probabilistic systems, and show that robustness does not increase the complexity of their model-checking…