Critical Observability for Automata and Petri Nets

TL;DR

This paper analyzes the computational complexity of determining critical observability in cyber-physical systems modeled as automata and Petri nets, revealing varying degrees of difficulty from efficient to undecidable.

Contribution

It provides a comprehensive complexity classification for critical observability across different system models, including automata and Petri nets.

Findings

Deciding critical observability is NL-complete for finite automata.

Deciding critical observability is PSPACE-complete for networks of automata.

Deciding critical observability is undecidable for labeled Petri nets, but decidable under certain conditions.

Abstract

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.