Keywords: Supervisory Control Theory, Performance evaluation, optimization, Tools
Abstract: Supervisory controllers are crucial for industrial cyber-physical systems to ensure their safe and efficient operations. Correct-by-construction supervisory controllers can automatically be generated from requirements using supervisory controller synthesis. Whilst formal synthesis techniques are well-established, their applications in real-world systems often suffer from scalability challenges. Rather than improving the synthesis algorithms and underlying data structures, this paper investigates how choices in modeling constructs affect synthesis performance. We propose a structured approach to identify modeling patterns that significantly hinder synthesis efficiency, analyze the cause of such bottlenecks, and resolve them in a generic manner to also benefit other practitioners. Drawing upon a collection of industrial models developed at ASML, we apply the approach to resolve two such bottlenecks, gaining remarkable improvements in synthesis time. By making our improvements available in the open-source Eclipse ESCET toolkit, these results directly benefit practitioners, further bridging the gap between theoretical synthesis and industrial development. Finally, our work shows that small changes in modeling can lead to significant differences in synthesis performance, and that there is still much to be gained by further investigations into synthesis performance bottlenecks, not just from an algorithmic perspective, but also from a modeling perspective.

Keywords: Performance evaluation, optimization, Tools, Automata
Abstract: State estimation is a fundamental technique in control theory and formal verification. A state estimator provides the set of all states that can be active after an observed sequence of events. Discrete event systems with real-time constraints, such as timed automata (TA), are notoriously complex and therefore difficult to analyze. In general, state estimation of TA is undecidable, and even for decidable subclasses, it remains computationally expensive. The literature presents several state estimation methods for different subclasses of TA. However, these methods are often introduced as theoretical results and are rarely evaluated in practice with respect to their computational resource requirements. This limits the comparability of these methods with regard to their practical applicability.

In this paper, we present a comparative analysis of five state-of-the-art state estimation methods. We have implemented these methods in an open-source software tool and conducted an extensive evaluation on 28 realistic models, derived from case studies in the literature. The models cover diverse domains, including smart home devices, automotive systems and network architectures. We compare the state estimation methods in terms of their computational efficiency and the expressiveness of the TA subclasses they support. Our results provide a comprehensive view of the practical applicability of state estimation methods for TA.

Keywords: Tools, Petri nets, Performance evaluation, optimization
Abstract: This paper presents a Timed Continuous Petri Net (TCPN)–based testbed for analyzing critical-traffic schedules in Time-Sensitive Networks (TSN). The testbed comprises three components: a bottom-up modeling methodology that captures the topology and behavioral characteristics of a TSN; logic control laws implementing the Time-Aware Shaper (TAS) gate control and enhanced scheduling mechanisms defined in IEEE~802.1Qbv; and a simulation and analysis module that computes performance indices, including schedule robustness under systematic variation of the Time Error (TE) ---a platform-dependent timing uncertainty whose estimate directly impacts schedule feasibility and resource utilization. A case study on clock offset induced by constant frequency drift demonstrates that the approach characterizes schedule tolerance beyond conventional feasibility checking.

Keywords: Automata, Verification, validation, test
Abstract: Isomorphic module systems constitute a distributed discrete-event modeling paradigm for large-scale multi-agent and networked architectures. They are composed of modules, instantiated from a given template, coordinated through global events. A key challenge is that even if the template is nonblocking or deadlock-free, the parallel composition of the modules may fail to satisfy these properties for some number of modules. The fundamental problem is to determine the maximum number of modules that can be safely composed while preserving nonblockingness or deadlock-freeness. We establish the computational complexity of the associated decision problems, proving that both problems are PSPACE-complete, and show that the minimal number m of modules that causes the system to become blocking or deadlocked can be found in time O(m2^m), which is bounded by O(n2ⁿ), where n is the number of states of the template, improving thus the known complexity of these problems.

Keywords: Supervisory Control Theory
Abstract: A unified formulation of controller synthesis for discrete event systems is presented, where both concepts from supervisory control, reactive systems, and game theory are joined in a common framework. It is based on transition systems, including both state and transition labels. An extended version of the temporal logic CTL*, which is strictly defined by mu-calculus, makes it possible to define both nonblocking, controllability, nondeterminism, and games in a unified way. It is also shown how modular temporal logic specifications can be introduced as an attractive alternative to traditional Buchi automata. This opens up for modular and incremental state-space reduction and efficient design of multi-agent systems.

Keywords: Petri nets, Automata, Applications
Abstract: In recent years the theory of Higher Dimensional Automata (HDA) has seen significant advances from a theoretical point of view, reflecting standard automata theory. There have also been first attempts to use the mathematical framework provided by HDAs to known problems, in particular Petri Net analysis. However real-world applications are still lacking and issues from real-world system, as concurrency, is still opened in the context of controller generation. In this work we show how the framework of HDAs can be adapted to help transforming controllers given as interpreted Petri nets (IPN) into an actual closed loop controller and how the HDA helps in identifying ambiguous or even contradictory specifications that remain “hidden” in the IPN. We demonstrate the feasibility by connecting the obtain controller to a virtual environment for closed loop control, exemplified by an industrial example.

Keywords: Supervisory Control Theory, Automata
Abstract: For modular discrete-event systems (DES) with shared uncontrollable and/or unobservable events, the modular closed-loop systems depend on the chosen decomposition of a specification, which is not the case if all shared events are controllable and/or observable. In this paper, our approach is based on maximal conditional decompositions of global specification languages. Such maximal decompositions then lead to less restrictive modular synthesis compared to the use of minimal (projection-based) decompositions. Another application of maximal decompositions is the construction of larger coobservable sublanguages in decentralized supervisory control compared to previous approaches.

Keywords: Petri nets, Identification
Abstract: The aim of this article is to synthesise Petri nets modelling the behaviour of synchronous or asynchronous systems. We then propose an active learning method for safe Petri nets, considering both interleaving semantics and maximal step semantics. Our method is based on active identification algorithms, such as L*, to determine the system language. We then propose a bolean satisfiability (SAT) modelling to determine the Petri nets that generate the identified language w.r.t. the chosen semantics.

Keywords: Cyber-security, Diagnosis, Verification, validation, test
Abstract: This paper considers decentralized diagnosability for discrete event systems under partial observation at multiple (local) observation sites, through the intersection of local state estimates. Each observation site is equipped with a processing node, which uses the sensor information it receives regarding underlying system activity (namely, events observable to this site), to perform (local) monitoring and obtain plausible estimates of the system states. The resulting (local) system state estimates are sent to a coordinator that is in charge of reaching a final assessment by performing appropriate set-intersection operations. We consider attacks that could affect one or more observation sites and cause the corruption of their sets of state estimates via deletions, insertions, or substitutions of observable events. Due to constraints on the attacker resources, we assume that the number of corrupted observation sites cannot exceed a natural number D (where D is less than or equal to the total number of observation sites). A structure is developed, called a D-tolerant verifier, to verify D-tolerant decentralized diagnosability based on a modified set-intersection operation of local state estimates at the coordinator. This allows us to systematically capture all possible behavior of a system under attacks (constrained to at most D corrupted sites) and assess the ability of the coordinator to reach proper diagnosis decisions despite the presence of tampering.

Keywords: Automata, Diagnosis, Observability
Abstract: This paper investigates deep faults diagnosis and diagnosability in the framework of timed discrete event systems under sensor failures and sensor attacks. For this purpose a non-deterministic dynamical observation mechanism is in troduced and analysed. A formal model of one clock timed automata, called clock interval automata, is used at modeling level to embed the timing aspects. Building on these models, deep faults are represented as timed faulty patterns. A recog nizer of the patterns under interest is first built by composing the system with the pattern and a diagnoser is then proposed based on a determinization process. Finally a diagnosis function as a diagnosability test is described and discussed. The main contribution is to provide diagnosis and diagnosability decisions for complex faults in timed and uncertain settings where some information are lost because of sensor failures or tampered because of sensor attacks. This framework thus contributes to improve the safety of cyber–physical systems.

Keywords: Automata, Diagnosis, Verification, validation, test
Abstract: Prognosability is a property that assesses whether faults can be predicted in advance based on a limited number of observation steps. However, it is inherently restrictive, as it requires all fault occurrences to be predictable. In large-scale and complex systems, certain fault scenarios are often intrinsically unpredictable due to limited sensor coverage, whereas others are well monitored. As a result, classical prognosability fails to capture the partial predictability exhibited by such systems. In this paper, we investigate a weaker version of prognosability, termed weak prognosability, which fills this gap by characterizing systems that can predict faults in specific scenarios (i.e., along certain strings), while distinguishing them from behaviors that are completely opaque to fault prediction. Specifically, we study the computational complexity and decidability of checking weak prognosability for automata and labeled Petri nets. We show that deciding weak prognosability is PSPACE-complete for automata, EXPSPACE-complete for modular automata, and undecidable for labeled Petri nets.

Keywords: Diagnosis, Automata, Observability
Abstract: This paper addresses the diagnosis of stuck faults in Stochastic Discrete-Event Systems—a class of failures that induce permanent structural changes by disabling specific transitions—through a computationally efficient approximation framework. Conventional monolithic approaches to this problem often suffer from state explosion. To overcome this limitation, we propose a Dual-Observer Bayesian Framework. Exploiting the natural decomposition of the faulty model into distinct nominal and post-fault dynamics, we decouple the state estimation problem and employ two parallel, lower-dimensional Belief Observers, thereby significantly reducing computational complexity. Furthermore, a novel reset mechanism is integrated into the Bayesian update logic. This mechanism resolves the Zero-Probability Reset by dynamically re-initializing the belief state upon detecting zero-likelihood observations, ensuring the diagnoser maintains continuous sensitivity to fault occurrences. The efficacy of the proposed framework is demonstrated through a numerical example.

Keywords: Applications, Discrete approaches for hybrid systems, Supervisory Control Theory
Abstract: Discrete-event systems and supervisory control theory provide a rigorous framework for specifying correct-by-construction behavior. However, their practical application to swarm robotics remains largely underexplored. In this paper, we investigate a topological recovery method based on discrete-event-systems within a swarm robotics context. We propose a hybrid architecture that combines a high-level discrete event systems supervisor with a low-level continuous controller, allowing lost drones to safely recover from fault or attack events and re-enter a controlled region. The method is demonstrated using ten simulated UAVs in the py-bullet-drones framework. We show recovery performance across four distinct scenarios, each with varying initial state estimates. Additionally, we introduce a secondary recovery supervisor that manages the regrouping process for a drone after it has re-entered the operational region.

Keywords: Discrete approaches for hybrid systems, Automata, Applications
Abstract: In recent years, automated climate control has been applied in greenhouses to achieve higher yields, better quality, and more efficient resource use. However, this control methodology simply adapted traditional building climatic control to the greenhouse context, without accounting for the effects of the plants within. In this paper, we transfer advanced modeling and control methodologies from systems engineering to maintain optimal temperature and CO2 levels for plant growth. In particular, we introduce hybrid automata and supervisory control theory to automatically synthesize controllers that not only account for the usual greenhouse thermal effect, but also for the presence of plants, whose CO2 absorption rate changes over time due to daylight-dependent photosynthesis and canopy growth. Simulation results confirm that the synthesized controllers maintain temperature and carbon fertilization level within the desired bounds.

Keywords: Applications, Synthesis Based Engineering, Discrete approaches for hybrid systems
Abstract: Supervisor synthesis is a well-known control solution for discrete-event systems. For hybrid systems, abstraction methods have been introduced to obtain a discrete-event model suitable for supervisor synthesis. However, their use in industrial applications remains scarcely documented. This paper describes the application of abstraction on a large-scale industrial system as part of the synthesis-based engineering process, demonstrates controller validation by software- and hardware-in-the-loop simulations based on historical data, and describes the insights gained.

Keywords: Supervisory Control Theory, Automata, Discrete approaches for hybrid systems
Abstract: This paper explores consensus control and stability in discrete-event networks governed by a supervisory Moore automaton that regulates interaction patterns. The dynamics in this study change only through event-triggered updates and automaton-driven switching, unlike continuous or hybrid multi-agent systems. Thus, we require stability tools specifically designed for logic-based state development. We develop a comparison framework using nonnegative matrices to establish global componentwise boundedness under arbitrary supervisory switching. This framework provides a relative stability guarantee based on the M-matrix criteria. Additionally, we establish a common copositive Lyapunov function to demonstrate that the network state converges globally and exponentially for all possible automata paths. A numerical case study demonstrates how discrete supervisory logic affects stability and cooperation in event-driven multi-agent systems, confirms the theoretical results, and shows how the automaton-supervised network behaves.