Model checking for complex temporal hyperlogics is decidable
Model Checking HyperRecHML is Decidable
Logic in Computer ScienceFormal Languages and Automata Theory
Summary
Checking whether certain complex time-based logic statements about multiple system runs are true has been a difficult open problem. The authors studied a very expressive logic called HyperRecHML that can mix different ways of describing these properties. They developed a method to simplify any such logic into a standard form and then created an algorithm that can determine if a system satisfies these properties. This shows that verifying these complex statements is actually possible and manageable despite their complexity.
What this means in practice
- •For runtime verification engineers: Enable efficient automated checks of complex temporal properties involving multiple executions during system monitoring.
- •For formal verification teams: Support building verification tools that handle more expressive specifications mixing fixed points and trace quantification.
Authors
Elli Anastasiadi, Kim Guldstrand Larsen, Martin Zimmermann
Abstract
Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.