Keywords: Cyber-security, Verification, validation, test, Automata
Abstract: One of the fundamental aspects of cybersecurity is the concept of confidentiality, which ensures that only authorized agents can access the system's sensitive data. Confidentiality can be achieved through encryption techniques implemented in the network application layer for discrete event systems. Although these techniques safeguard the confidentiality of information, they rely on synchronized communication between the sender and the receiver. In some cases, transient communication failures can occur due to external interference, and the network always recovers within a short period. If a package is lost during transmission, the receiver will be unable to decipher any subsequent communications. Thus, to address this issue, we investigate the robustness of detectability against communication losses in ciphered discrete event systems. Since communication loss is transient, we assume that, in a given network, up to k events can be lost in sequence and that, if a new event is successfully transmitted after a communication loss, the next l-1 events are sure to be transmitted to the receiver. In this sense, we formulate the problem of robust detectability against transient communication failures, leading to the k-loss l-assured detectability property. To verify this property, we show that it can be reduced to a determined number of (k₁,k₂)-detectability instances, for which verification has been shown in the literature to be polynomial in the size of the plant model.

Keywords: Automata, Cyber-security, Discrete event simulation
Abstract: Cyber-physical systems (CPS) that rely on networked sensing and actuation are vulnerable to cyberattacks that can compromise their safety and availability. We address this challenge for discrete-event systems (DES)-CPS modeled as finite-state automata (FSA). We focus on two network attack models: actuator-enablement (AE) and sensor-deception (SD). AE attacks induce a system to perform unauthorized or unsafe actions, whereas SD attacks mislead a system by supplying falsified measurements. As part of the defense mechanism, we introduce inspection states as designated checkpoints that segment closed-loop executions into inter-inspection substrings. We also define a damage model in which occurrence of attacked or propagated events accumulates cost toward state-dependent damage budgets. Based on the system model, we define a quality automaton that captures the evolution between successive inspections and distinguishes operational from faulty modes. On this basis, we define worst-case inter-inspection damage and damage ranges for each attack class and derive conditions under which a supervisor with a given inspection placement is AE- or SD-attack resilient. We provide language-theoretic metrics and design criteria that bound undetected damage without detailed assumptions on the adversary.

Keywords: Petri nets, Verification, validation, test
Abstract: We study the secret protection problem (SPP), where the objective is to find a policy of minimal cost ensuring that every execution path from an initial state to a secret state contains a sufficient number of protected events. The problem was originally introduced and studied in the setting of finite automata. In this paper, we extend the framework to labeled Petri nets. We consider two variants of the problem: the Parikh variant, where all occurrences of protected events along an execution path contribute to the security requirement, and the indicator variant, where each protected event is counted only once per execution path. We show that both variants can be solved in exponential space for labeled Petri nets, and that their decision versions are EXPSPACE-complete. As a consequence, there is no polynomial-time or polynomial-space algorithm for these problems.

Keywords: Petri nets, Supervisory Control Theory
Abstract: This work revisits the problem of forbidden-state supervisory control for safe Petri nets, using Boolean algebra as the basic representational and analytical framework. The presented analysis systematizes and generalizes related past results in the Petri net literature, and pronounces the salient structure that underlies these developments. Furthermore, the computation involved in the presented methodology can be facilitated by well-developed algorithms and software tools for the processing and the simplification of the Boolean functions involved, and it is naturally amenable to incremental, iterative schemes that enable learning processes.

Keywords: Applications, Tools, Verification, validation, test
Abstract: The majority of tools supporting modelling and analysis of discrete event controllers and supervisors do not provide code generation. Then, the translation of the model into executable code should be done by hand. This is one of the main issues for the application in practice of the theoretical results presented in the last decades in this field. Moreover, the cost for developing an environment offering code generation for off-the-shelf devices is not negligible, also because the number of these devices is high. To solve this issue, this paper presents an approach centered on Stateflow charts, for which Simulink already supports code generation for several off-the-shelf devices.

Keywords: Tools, Supervisory Control Theory
Abstract: Supervisory control theory (SCT) of discrete-event systems is a mature theoretical framework with broad applications. This paper presents PiTCT, an open-source Python toolbox that provides easy and script-based access to classical SCT computation. PiTCT is designed as a Python extension of an established automaton-based control tool, exposing fundamental DES modeling, analysis, and supervisor synthesis operations through a lightweight Python interface. By embedding these operations in Python, PiTCT integrates naturally with widely used scientific and visualization packages and supports reproducible, notebook-based workflows. To further lower the entry barrier, PiTCT is distributed via PyPI and is also available through a browser-based JupyterLite service with no local installation required. The paper demonstrates the main features of PiTCT through a running printer example, illustrating how classical SCT concepts can be directly implemented in codes.

Keywords: Synthesis Based Engineering, Petri nets, Tools
Abstract: Controller synthesis for cyber-physical systems is a powerful technique to ensure safe and correct behavior, yet its application in industrial settings remains limited. Its adoption is hindered by practical issues, such as the lack of specialized tooling, unfamiliar specification languages, and modeling paradigms that differ from engineers' established workflows. We present SynthML, a tool that addresses these challenges by integrating synthesis-based engineering into existing practices: it automatically synthesizes UML activities, a widely used modeling formalism in industry, from abstract specifications also expressed in UML. The activity synthesis algorithm combines supervisory controller synthesis with Petri net synthesis to capture concurrency, and computes control flow guards to ensure that any activity execution adheres to the synthesized controlled behavior. This multi-step algorithm provides correct-by-construction, deadlock-free, and maximally-parallelized UML activities, presented in a familiar UML notation that intuitively represents concurrent behavior.

Keywords: Automata, Supervisory Control Theory, Synthesis Based Engineering
Abstract: SUPREMICA and ESCET are two tools that both support modeling discrete event systems by extended finite-state machines, which are finite-state automata extended with bounded discrete variables and guards and actions over those variables. Both tools implement efficient algorithms for verification and synthesis of supervisors according to the Ramadge and Wonham supervisory control theory. But the tools are not identical, and they excel in different areas of functionality, which makes it useful to be able to convert models between them. One distinction between them is that SUPREMICA uses a graphical interface, while ESCET uses a textual representation given in the CIF language. Conversion from CIF to SUPREMICA is readily available from within ESCET, and this paper describes the conversion from SUPREMICA to CIF implemented as a script within SUPREMICA. This conversion is not as straightforward as would first be thought, due to multiple idiosyncrasies of the two formats of extended finite-state machine representation.

Keywords: Discrete approaches for hybrid systems
Abstract: In this talk, I will present recent advances in (data-driven) verification and control synthesis for both linear and nonlinear stochastic models. I will first discuss how approximate stochastic simulation relations can be exploited to reduce the complexity of model-checking problems, enabling scalable formal verification of systems with uncertainty.

In many practical scenarios, exact knowledge of a system’s dynamics is unavailable—whether due to incomplete modeling of the physical components and their environment, or due to degradation and changes during operation. To address this challenge, I will show how controllers can still be systematically designed and formally verified using data-driven techniques. These methods allow us to guarantee correct behavior with minimal assumptions on the underlying model, bridging the gap between theoretical rigor and real-world applicability. Profile

Keywords: Petri nets, Applications, Scheduling
Abstract: Abstract—Multi-Agent Path Finding (MAPF) requires collision-free trajectories for multiple agents on a shared graph, often with the objective of minimizing the sum-of-costs (SOC). Many optimal and bounded-suboptimal solvers rely on time-expanded models and centralized conflict resolution, which limits scalability in large or dense instances. We propose a hybrid prioritized framework that separates geometric planning from execution-time conflict resolution. In the first stage, Geometric Conflict Preemption (GCP) plans agents sequentially with A* on the original graph while inflating costs for transitions entering vertices used by higher-priority paths, encouraging spatial detours without explicit time reasoning. In the second stage, a Decentralized Local Controller (DLC) executes the geometric paths using per-vertex FIFO authorization queues and inserts wait actions to avoid vertex and edge-swap conflicts. Experiments on standard benchmark maps with up to 1000 agents show that the method scales with an near-linear runtime trend and attains a 100% success rate on instances satisfying the geometric feasibility assumption. Page of the project: https://sites.google.com/unizar.es/multi-agent-path-finding/home

Keywords: Petri nets, Applications, Synthesis Based Engineering
Abstract: We study supervisory control of heterogeneous multi-robot teams executing collaborative activities specified by Linear Temporal Logic (LTL). A central challenge is capturing the cross-robot synchronization required by joint activities without constructing the global synchronous product of all robot models, which leads to state explosion. We propose a framework based on synchronized place-transition Petri nets with outputs: each robot class is modeled by a compact P/T net, and inter-class coordination is realized at execution time through shared synchronization events. A marking-based output interface produces observations for a supervisor derived from a Büchi automaton of the mission, while the supervisor issues (i) activity-start commands and (ii) marking-target commands that are delegated to a motion planner. The approach stays within standard P/T nets, avoids explicit global state construction at modeling time, and enables the use of structural Petri-net techniques for feasibility analysis, under an explicit assumption on the realizability of marking-target commands by the motion planner.

Keywords: Scheduling, Performance evaluation, optimization
Abstract: To maximize performance in modern production environments, there is a trend toward integrating multiple systems from different vendors into production lines. Scheduling work in such lines requires careful coordination of the machines' operational states. Achieving optimal schedules involves considering the duration of operations, travel, and sequence-dependent setup -- factors that are critical in a high-mix low-volume (HMLV) setting due to the variability in job requirements. We present a methodology for scheduling HMLV production lines that explicitly considers these time constraints. The approach employs a modular domain model to describe the production line and the diverse set of operations it must perform. Domain model specifications are translated into a constraint graph, which enables efficient computation of a shortest feasible production line schedule. To demonstrate our methodology, we apply it to a production scenario inspired by the professional printing domain. The results illustrate the applicability of the approach to production environments in which flexibility and responsiveness are essential.

Keywords: Performance evaluation, optimization, Supervisory Control Theory, Applications
Abstract: This paper introduces a hybrid stochastic planning and predictive control strategy for multi-agent coordination that enables decentralization while preserving the formal safety guarantees inherent in centralized supervisory control. The approach integrates Supervisor Localization to embed safety constraints into agent-level supervisors, Markov Decision Processes (MDPs) for local performance optimization under uncertainty, and a stochastic consensus protocol to synchronize distributed event probability with communication delays. By employing a receding-horizon MDP that updates policies online based on dynamically refined stochastic models, the strategy supports autonomous and adaptive decision-making without centralized oversight. Validation through a case study of heterogeneous autonomous robots under resource constraints demonstrates that the framework maintains safety, ensures probabilistic coordination, and achieves near centralized performance, thereby unifying formal discrete-event control with scalable, resilient multi-agent autonomy.

Keywords: Discrete event simulation, Automata, Verification, validation, test
Abstract: Caring for elderly individuals in their homes requires significant time and resources from healthcare workers, particularly as the ageing population grows. Smart homes are increasingly being deployed worldwide, and utilizing binary sensors installed in these homes to monitor residents’ daily activities could assist healthcare professionals. This paper employs existing user activity data in the form of probabilistic graphs combined with medical staff recommendations to propose a personalized daily activity program. To achieve this, variants of Linear Temporal Logic (LTL), including Counting Time Temporal Logic and One-Clock Metric Temporal Logic, will be implemented in different solvers. These solvers will traverse the graph, applying constraints to determine the most likely activity sequence for each user. A case study will be presented and analyzed to validate this approach.

Keywords: Max/plus-algebra
Abstract: Max-min-plus-scaling (MMPS) systems extend max-plus and max-min-plus models by incorporating a scaling operation, making them suitable for modeling discrete-event systems involving timing, synchronization, and resource constraints. This paper focuses on implicit MMPS systems, where the current state depends on itself, which complicates analysis because solutions may not exist or may be non-unique. We investigate conditions under which such systems are solvable. We prove that the implicit MMPS system is solvable if the corresponding implicit interconnection graph does not contain any circuits. When there exist a circuit, we develop necessary and sufficient conditions for the system to be solvable. The paper also discusses solvable regions and proposes an iterative method for computing system states. We demonstrate all the theoretical results with a numerical example.

Keywords: Discrete approaches for hybrid systems, Max/plus-algebra, Petri nets
Abstract: This paper investigates reachability analysis for max-plus linear systems (MPLS), an important class of dynami- cal systems that model synchronization and delay phenomena in timed discrete-event systems. We specifically focus on backward reachability analysis, i.e., determining the set of states that can reach a given target set within a certain number of steps. Computing backward reachable sets presents significant challenges due to the non-convexity of max-plus dynamics and the complexity of set complement operations. To address these challenges, we propose a novel approximation framework that efficiently computes backward reachable sets by exploiting the structure of tropical polyhedra. Our approach reformulates the problem as a sequence of symbolic operations and approximates non-convex target sets through closure operations on unions of tropical polyhedra. We develop a systematic algorithm that constructs both outer (M-form) and inner (V-form) represen- tations of the resulting sets, incorporating extremal filtering to reduce computational complexity. The proposed method offers a scalable alternative to traditional DBM-based approaches, enabling reliable approximate backward reachability analysis for general target regions in MPLS.

Keywords: Max/plus-algebra, Tools
Abstract: This paper investigates the growth rate and fixed points of periodic max-min-plus-scaling (MMPS) systems with a period greater than one. First, we analyze the average growth rate of the periodic MMPS system by introducing an extended periodic form for the MMPS system. Then we propose a tree search algorithm to calculate the average growth rate of the periodic MMPS system with shorter execution time as compared to similar existing algorithms for MMPS systems.

Keywords: Discrete event simulation, Max/plus-algebra, Petri nets
Abstract: This work addresses the modeling and optimization of emergency hospital systems under overcrowding and resource constraints. An integrated framework is proposed, combining an analytical Markov chain model derived from the Petri net reachability tree with stochastic simulation based on Max-Plus algebra. Three scenarios are analyzed: an uncontrolled network, a deterministically controlled network, and a network with an optimized controller. The latter is formulated as a multiobjective optimization problem to maximize service rate and minimize system congestion. Performance is assessed in terms of throughput, patient occupancy, and staffing requirements. The results provide a unified perspective for decision support in emergency department planning and resource sizing.

Keywords: Max/plus-algebra, Cyber-security, Petri nets
Abstract: This paper addresses the resilience of Max-Plus Linear Systems under sensor timestamp-delay attacks, in which malicious delays are injected into event time measurements. Such attacks affect the temporal information available to the controller without altering the physical structure of the system. Building on a previous formulation that focused on innocuous attacks, we study a relaxed resilience notion based on semimodule invariance. We show that, although the closed-loop operator is monotone with respect to delay parameters, invariance is generally not monotone. This limitation stems from structural properties of max-plus semimodules and challenges the definition of a maximal admissible delay bound.

Keywords: Observability, Automata
Abstract: A recent series of papers introduced and investigated a novel state-estimation problem for a class of partially observable continuous-time transition models where the occurring events at the visited states are triggered according to exponential races among the corresponding enabled events. The current work provides an alternative analysis for this problem using a uniformization approach inspired by the classical Markov chain theory. The derived result simplifies and further systematizes the involved computation, while unveiling and pronouncing the essential structure of the process that drives the underlying dynamics with respect to the shaping of the obtained estimates.

Keywords: Supervisory Control Theory, Observability
Abstract: In the inference-based decentralized supervisory control framework for discrete event systems, multiple local supervisors perform multi-level inference against self-ambiguity and ambiguities of the others to jointly arrive at a correct control decision. For a chosen nonnegative integer N, the notion of N-inference observability together with controllability guarantees that the given specification language is enforced using N-level inference. The class of N-inference observable languages increases strictly monotonically as the parameter N is increased, i.e., there is no upper bound for the required level of inference. Informed by this fact, we introduce a notion of non-uniformly bounded inference observability, which does not involve an upper bound of inference level, and is weaker than N-inference observability for any nonnegative integer N. It together with controllability serves as a necessary and sufficient condition for the existence of a decentralized supervisor that uses inference with unbounded level.

Keywords: Opacity, Automata, Cyber-security
Abstract: Cyber-physical systems (CPS) are key elements in Industry 4.0, integrating physical components with monitoring and control devices through communication networks. Since communication networks are used, the transmitted information is subject to eavesdropping attacks, where the attacker may try to infer the system secret by observing the events transmitted on the attacked networks. In the context of Discrete-Event Systems, the security of information has been associated in the literature with the property of opacity. In this regard, considering that the secret information is represented by secret states of the plant, a system is said to be current-state opaque if the intruder is never capable of inferring a secret state based on the observation of events communicated through the attacked networks. Thus, security mechanisms must be used to enforce current-state opacity. One of the strategies usually adopted in cyber-protected industrial systems is network segmentation into isolated smaller sub-networks (subnets), aiming to limit lateral movements of attackers, to protect critical assets, and to reduce the overall attack surface of a given system. In this paper, we propose a strategy for network segmentation which ensures that the system is current-state opaque with respect to the observation of the events that are transmitted through each subnet individually. Thus, if the attacker invades any subnet, they will not be able to observe any events transmitted by other subnets, nor will they be able to infer that the system has reached a secret state.

Keywords: Opacity, Automata, Verification, validation, test
Abstract: This paper investigates two variants of k-tail opacity in discrete event systems. The ``k-tail'' refers to the most recent portion of a system run, defined as its longest suffix containing at most k steps. We distinguish between k-observation tail opacity, where the steps are counted in terms of observable events, and k-event tail opacity, where the steps are counted by considering all events regardless of observability. Both properties ensure that an intruder cannot infer whether a secret state was visited in the last k steps. For the verification of the two types of k-tail opacity, we introduce two novel approaches that rely on k-observation and k-event secret verifiers, respectively.

Keywords: AI-integration in DES, Supervisory Control Theory, Performance evaluation, optimization
Abstract: The control of autonomous multi-robot 3D construction systems faces a fundamental trade-off between enforcing safety and correctness and achieving efficient task execution. Supervisory Control Theory (SCT) enables the construction of safe/correct-by-construction supervisors, but they typically fail to prescribe how actions should be selected from a set of enabled actions. On the other side, Reinforcement Learning (RL) is a well-suited machine learning technique for sequential decision-making and performance optimization, but it does not provide guarantees for safety or correctness. This work shows how parallel advantages can be taken from SCT and RL and applied to multi-robot 3D construction. Our approach intelligently selects its actions among those enabled by an SCT supervisor, minimizing the total number of actions required to complete construction tasks while formally guaranteeing correctness. Its feasibility is illustrated through simulations in 3D construction scenarios with multiple robots, showing significant reductions in the number of actions compared to pure SCT supervisors and greedy policies.

Keywords: AI-integration in DES, Verification, validation, test, Automata
Abstract: Manufacturing industries are facing increasing product variability due to the growing demand for personalized products. Under these conditions, ensuring safety becomes challenging as frequent reconfigurations can lead to unintended hazardous behaviors. Multi-agent control architectures have been proposed to improve flexibility through decentralized decision-making and coordination. However, these architectures are based on predefined task models, which limit their ability to adapt task planning to new product requirements while preserving safety. Recently, large language models have been introduced into manufacturing systems to enhance adaptability, but reliability remains a key challenge. To address this issue, we propose a control architecture that leverages the flexibility of large language models while preserving safety on the manufacturing shop floor. Specifically, the proposed framework verifies large language model-enabled task allocations by using temporal logic and discrete event systems. The effectiveness of the proposed framework is demonstrated through a case study that involves a multi-robot assembly scenario, showing that unsafe tasks can be allocated safely before task execution.

Keywords: AI-integration in DES, Supervisory Control Theory, Automata
Abstract: We study the synthesis of synchronous communication protocols for decentralized discrete-event control from a reinforcement-learning perspective. Instead of evaluating protocols only through structural notions such as logical minimality, we introduce a communication-augmented verification model that allows us to study how learned communication policies are used during system operation. Using this model, we formulate protocol synthesis under partial observation as an independent Q-learning problem based on local information. This approach results in feasible local communication policies. Examples show that reward design can affect which correct protocol is learned.

Keywords: AI-integration in DES, Supervisory Control Theory, Fault tolerance
Abstract: Supervisory control of discrete-event systems provides formal guarantees of correctness with respect to a plant model and specification. However, these guarantees heavily rely on the plant model, which can deviate from nominal behavior due to modeling errors or faults. Recent notions of discrete robustness model deviations as a set of additional transitions thatcan be added to the plant. The discrete robustness is defined as all sets of extra transitions for which the supervised system still guarantees a desired specification. However, this notion suffersfrom scalability due to the large solution space and conservatism since most deviations are infeasible in practice. This paper proposes to address these two issues using a neurosymbolic computing framework for discrete robustness analysis of safety properties. First, a neural reasoning layer based on Large Language Models infers a set of feasible deviation transitions from system models, specifications, and domain knowledge. Next, a symbolic layer computes the discrete robustness guarantees over the inferred deviation set. We evaluate our framework on three case studies, demonstrating that our method identifies a smaller set of feasible deviations while preserving robustness guarantees comparable to those of full transition-based analysis.