Critical Observability for Automata and Petri Nets
This work provides a complexity-theoretic characterization of critical observability for discrete-event systems, aiding system designers in understanding the feasibility of verification.
The paper establishes the computational complexity of deciding critical observability for systems modeled as finite-state automata and Petri nets, showing it is NL-complete for finite automata, PSPACE-complete for networks of finite automata, and undecidable for labeled Petri nets (decidable with finite or co-finite critical states, as hard as non-reachability).
Critical observability is a property of cyber-physical systems to detect whether the current state belongs to a set of critical states. In safety-critical applications, critical states model operations that may be unsafe or of a particular interest. De Santis et al. introduced critical observability for linear switching systems, and Pola et al. adapted it for discrete-event systems, focusing on algorithmic complexity. We study the computational complexity of deciding critical observability for systems modeled as (networks of) finite-state automata and Petri nets. We show that deciding critical observability is (i) NL-complete for finite automata, that is, it is efficiently verifiable on parallel computers, (ii) PSPACE-complete for networks of finite automata, that is, it is very unlikely solvable in polynomial time, and (iii) undecidable for labeled Petri nets, but becoming decidable if the set of critical states (markings) is finite or co-finite, in which case the problem is as hard as the non-reachability problem for Petri nets.