Counting and sliding verifying and restoring healthy systems

Abstract

Reactive systems play a significant role in the daily life of every person. Such systems include personal computers, automatic teller machines, devices we use every day in our households, and also systems that play a less active but still important role, for example monitoring devices scanning for environmental threats in a country. In particular for safety-critical reactive systems it is of enormous importance that correctness properties of such systems have been verified. A very prominent technique to tackle such verification tasks is called model checking. From a theoretical point of view, model checking commonly boils down to solving classical decision problems for finite automata; usually automata operating on infinite words. We study Parikh automata on finite and infinite words with applications to model checking. These automata extend classical finite automata with a Counting mechanism. Still, due the dynamics of the realworld it might be the case that a change in the environmentleads to a faulty or even dangerous state of such a system. Referring to the above example of devices scanning for environmental threats, assume that due to a mistake at a local construction site the connection to the other devices has been cut, leaving a part of the country unmonitored. Hence, a new solution has to be computed. However, the new solution can differ arbitrarily from the current state. Given that it is costly to move such devices around, it is desirable to compute a new solution that is close to the current state. To capture and formalize such scenarios, we introduce the new framework of solution discovery via reconfiguration for constructing a feasible solution for a given problem by executing a sequence of small modifications starting from a given state.