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.

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