Model checking LTL over controllable linear systems is decidable

DOI10.1007/3-540-36580-X_36MaRDI QIDQ4418864zbMATH OpenFDO

Authors George Pappas, Paulo Tabuada

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2623/26230498.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Linear systems in control theory (93C05) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Recommendations

• LTLC: Linear Temporal Logic for Control
• Language-guided controller synthesis for discrete-time linear systems
• Hybrid Systems: Computation and Control
• Decidable controller synthesis for classes of linear systems
• The algorithmic analysis of hybrid systems

Cited in

(21)

• Bisimilar linear systems.
• Verification of a technical system model with linear temporal logic
• Monitoring bounded LTL properties using interval analysis
• GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
• LTLC: Linear Temporal Logic for Control
• Algorithmic metatheorems for decidable LTL model checking over infinite systems
• Decidable controller synthesis for classes of linear systems
• Towards efficient exact synthesis for linear hybrid systems
• scientific article; zbMATH DE number 7559425 (Why is no real title available?)
• On the decidability of linear bounded periodic cyber-physical systems
• Automated Technology for Verification and Analysis
• Hybrid Systems: Computation and Control
• Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
• A bounded model checking technique for discrete-time nonlinear systems
• Fully automated verification of linear time-invariant systems against signal temporal logic specifications via reachability analysis
• Hybridization methods for the analysis of nonlinear systems
• Symbolic models for control systems
• Modal specifications for the control theory of discrete event systems
• Temporal logic model predictive control
• Multi-modal control using adaptive motion description languages
• Inclusion dynamics hybrid automata

This page was built for publication: Model checking LTL over controllable linear systems is decidable

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4418864)