On the synthesis of discrete controllers for timed systems

DOI10.1007/3-540-59042-0_76zbMath1379.68227OpenAlexW2144965436MaRDI QIDQ4596624

Joseph Sifakis, Amir Pnueli, Oded Maler

Publication date: 4 December 2017

Published in: STACS 95 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-59042-0_76

Mathematics Subject Classification ID

Applications of game theory (91A80) Formal languages and automata (68Q45) Synthesis problems (93B50) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20)

Related Items (78)

Automatic synthesis of a subclass of schedulers in timed systems. ⋮ New Results on Timed Specifications ⋮ Scheduling with timed automata ⋮ Robust Specification of Real Time Components ⋮ Minimum Attention Controller Synthesis for Omega-Regular Objectives ⋮ Crossing the Bridge between Similar Games ⋮ Graph Games and Reactive Synthesis ⋮ Model Checking Real-Time Systems ⋮ Symbolic Model Checking in Non-Boolean Domains ⋮ Using logic to solve the submodule construction problem ⋮ From finite automata toward hybrid systems (Extended abstract) ⋮ Compositional and symbolic synthesis of reactive controllers for multi-agent systems ⋮ Controller synthesis for hybrid systems with a lower bound on event separation ⋮ Controller/Orchestrator Synthesis via Filtration ⋮ Dynamic controllability via timed game automata ⋮ Optimal paths in weighted timed automata ⋮ On the relation between reactive synthesis and supervisory control of non-terminating processes ⋮ Robust synthesis for real-time systems ⋮ Automatic synthesis of switching controllers for linear hybrid systems: safety control ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ A survey of timed automata for the development of real-time systems ⋮ Modularity for timed and hybrid systems ⋮ Symbolic models for stochastic switched systems: A discretization and a discretization-free approach ⋮ Symbolic synthesis of masking fault-tolerant distributed programs ⋮ Temporal Robustness of Stochastic Signals ⋮ Games for synthesis of controllers with partial observation. ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ Controller synthesis for dynamic hierarchical real-time plants using timed automata ⋮ A survey of stochastic \(\omega \)-regular games ⋮ Timed Control with Observation Based and Stuttering Invariant Strategies ⋮ Compatibility of refining and controlling plant automata with bisimulation quotients ⋮ Synthesizing bounded-time 2-phase fault recovery ⋮ Dynamic controllability of temporal networks with instantaneous reaction ⋮ Robust supervisory control of timed discrete event systems under partial observation based on eligible time bounds: the existence conditions ⋮ Discrete-time control for rectangular hybrid automata ⋮ Specifications for decidable hybrid games ⋮ Zeno hybrid systems ⋮ Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets ⋮ On Scheduling Policies for Streams of Structured Jobs ⋮ Cancer hybrid automata: model, beliefs and therapy ⋮ Approximately bisimilar symbolic models for randomly switched stochastic systems ⋮ Lazy Abstraction-Based Controller Synthesis ⋮ Hybrid automata with finite bisimulations ⋮ Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\) ⋮ Backward symbolic optimal reachability in weighted timed automata ⋮ Viable set computation for hybrid systems ⋮ Interface synthesis and protocol conversion ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ A control synthesis approach for time discrete event systems ⋮ Grid automata and supervisory control of dense real-time discrete event systems ⋮ Solving games via three-valued abstraction refinement ⋮ Supervisory control of hybrid systems based on model abstraction and guided search ⋮ Compositional synthesis of finite abstractions for networks of systems: a small-gain approach ⋮ Methodologies for Specification of Real-Time Systems Using Timed I/O Automata ⋮ Unnamed Item ⋮ Verifying untimed and timed aspects of the experimental batch plant ⋮ Symbolic models for retarded jump-diffusion systems ⋮ STORMED Hybrid Games ⋮ Logical time control of concurrent DES ⋮ Optimal work-conserving scheduler synthesis for real-time sporadic tasks using supervisory control of timed discrete-event systems ⋮ A method for the modular synthesis of controllers for timed discrete-event systems ⋮ Robust safety of timed automata ⋮ A game approach to the parametric control of real-time systems ⋮ Synthesis of secure adaptors ⋮ Synthesis of Non-Interferent Timed Systems ⋮ Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation ⋮ Realizability of Real-Time Logics ⋮ Structural measures for games and process control in the branch learning model ⋮ Formal Synthesis of Real-Time Embedded Software by Time-Memory Scheduling of Colored Time Petri Nets1 1This work was partially supported by research project grant NSC-90-2215-E-194-009 from the National Science Council, Taiwan, ROC. ⋮ Conditional simple temporal networks with uncertainty and decisions ⋮ Discrete-time control for rectangular hybrid automata ⋮ Learning to win process-control games watching game-masters ⋮ Non-Interference Control Synthesis for Security Timed Automata ⋮ Timed games with bounded window parity objectives ⋮ Weak, strong, and strong cyclic planning via symbolic model checking ⋮ The complexity of automated addition of fault-tolerance without explicit legitimate states ⋮ A turn-based approach for qualitative time concurrent games ⋮ A supervisory control method for ensuring the conformance of real-time discrete event systems

This page was built for publication: On the synthesis of discrete controllers for timed systems