Papers for

runtime verification engineers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Model checking for complex temporal hyperlogics is decidable

Model Checking HyperRecHML is Decidable

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.

Thu 15 OctLogic in Computer ScienceFormal Languages and Automata Theory
The gist
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.
Open → 2610.21379v1

Policy changes in runtime monitors for long systems are complex

Policy Change for Treelike Monitors

Abstract: We study the policy change problem that arises in the runtime verification of long-running systems. The online monitors typically used in this context are generally treelike, in that they maintain substates that monitor subformulae of the target policy. We consider when and how the policy can be changed while the monitored system is running by only exploiting the information stored in the monitor's state. This is relevant, for example, to account for new system functionality or changes in regulatory requirements. We formally define the policy change problem in a general setting, independent of any specific (treelike) monitor implementation. We then show that policy change for past-time metric temporal logic (pMTL) is decidable but has tight non-primitive recursive lower and upper bounds, while with discrete-time semantics it is EXPSPACE-complete.

Wed 9 SeptLogic in Computer Science
The gist
Long-running computer systems often need to be checked constantly to make sure they follow important rules. The paper looks at how we can change these rules while the system is running, using just the information the monitor already has. The researchers found that deciding whether such changes can be made is very complicated, and they describe the exact limits of this complexity. They also show that when time is divided into steps, the problem is still very hard, but it's solvable within certain extreme computational bounds.
Open → 2609.10114v1