Symbolic reachability analysis and maximally permissive entrance control for globally synchronized templates

DOI10.1016/j.automatica.2017.10.015zbMath1378.93021OpenAlexW2767526152MaRDI QIDQ680540

Liyong Lin, Weilin Wang, Rong Su, W. Murray Wonham, Alin Stefanescu

Publication date: 23 January 2018

Published in: Automatica (Search for Journal in Brave)

Full work available at URL: https://hdl.handle.net/10356/137871

zbMATH Keywords

blockingsupervisor synthesisdeadlockparameterized discrete-event systemssymbolic reachability analysis

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65) Synthesis problems (93B50) Attainable sets, reachability (93B03)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Control of parameterized discrete event systems
• A Kleene characterization of computability
• Discrete-event modeling of multi-agent systems with broadcasting-based parallel composition
• Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk).
• On Distributed and Parameterized Supervisor Synthesis Problems
• Weak Invariant Simulation and Its Application to Analysis of Parameterized Networks
• Parameterized Model Checking of Rendezvous Systems
• The Verification and Control of Interacting Similar Discrete-Event Systems
• Iteration of rational transductions
• Regular Model Checking using Widening Techniques
• Predicates and predicate transformers for supervisory control of discrete event dynamical systems
• CONCUR 2004 - Concurrency Theory
• Computer Aided Verification
• Blocking in Fully Connected Networks of Arbitrary Size
• Computer Aided Verification