Counting and sliding verifying and restoring healthy systems

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.