Symbolic model checking for real-time systems
From MaRDI portal
Publication:1327398
DOI10.1006/INCO.1994.1045zbMath0806.68080OpenAlexW2130773092MaRDI QIDQ1327398
Joseph Sifakis, Thomas A. Henzinger, Xavier Nicollin, Sergio Yovine
Publication date: 13 February 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://hdl.handle.net/1813/6182
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (only showing first 100 items - show all)
Removing ε-transitions in timed automata ⋮ Unnamed Item ⋮ Model-checking for real-time systems ⋮ Verification in continuous time by discrete reasoning ⋮ Modularity for timed and hybrid systems ⋮ The tail-recursive fragment of timed recursive CTL ⋮ Automated repair for timed systems ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ A space-efficient on-the-fly algorithm for real-time model checking ⋮ Timed P Automata ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Progress-preserving Refinements of CTA ⋮ MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS ⋮ Model Checking Biological Oscillators ⋮ Combining qualitative information and semi‐quantitative data for guaranteed invalidation of biochemical network models ⋮ Weakest Invariant Generation for Automated Addition of Fault-Tolerance ⋮ The Unmet Challenge of Timed Systems ⋮ A menagerie of timed automata ⋮ Testing timed automata ⋮ Symbolic reachability computation for families of linear vector fields ⋮ Proving sequential function chart programs using timed automata ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ An Introduction to Timed Automata ⋮ Model-checking Timed Temporal Logics ⋮ A game approach to the parametric control of real-time systems ⋮ ON REACHABILITY AND SAFETY IN INFINITE-STATE SYSTEMS ⋮ Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets ⋮ Uniformity for the decidability of hybrid automata ⋮ Presburger liveness verification of discrete timed automata. ⋮ Adequacy and complete axiomatization for timed modal logic ⋮ Scheduling with timed automata ⋮ Efficient timed model checking for discrete-time systems ⋮ Symbolic model checking for probabilistic timed automata ⋮ Performance Evaluation of Schedulers in a Probabilistic Setting ⋮ An iterative approach to verification of real-time systems ⋮ The mu-calculus and Model Checking ⋮ Model Checking Real-Time Systems ⋮ Formal verification of real-time systems with preemptive scheduling ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ How to stop time stopping ⋮ Schedulability of asynchronous real-time concurrent objects ⋮ Model checking of time Petri nets using the state class timed automaton ⋮ Time-abstracted bisimulation: Implicit specifications and decidability ⋮ Tropical Fourier–Motzkin elimination, with an application to real-time verification ⋮ Event algebra for transition systems composition application to timed automata ⋮ Causality problem in real-time calculus ⋮ Reachability analysis of dynamical systems having piecewise-constant derivatives ⋮ Axiomatisation and decidability of multi-dimensional Duration Calculus ⋮ SetExp: a method of transformation of timed automata into finite state automata ⋮ Polynomial interrupt timed automata: verification and expressiveness ⋮ Weak bisimulation for probabilistic timed automata ⋮ Robust synthesis for real-time systems ⋮ Nested Timed Automata with Frozen Clocks ⋮ A theory of discontinuities in physical system models ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ Symbolic synthesis of masking fault-tolerant distributed programs ⋮ Verification in loosely synchronous queue-connected discrete timed automata. ⋮ Generalized discrete timed automata: Decidable approximations for safety verification. ⋮ Pushdown timed automata: A binary reachability characterization and safety verification. ⋮ Controller synthesis for dynamic hierarchical real-time plants using timed automata ⋮ Model-checking timed automata with deadlines with Uppaal ⋮ Verification and control of partially observable probabilistic systems ⋮ Dealing with practical limitations of distributed timed model checking for timed automata ⋮ Superposition as a decision procedure for timed automata ⋮ Modal event-clock specifications for timed component-based design ⋮ Reachability analysis for timed automata using max-plus algebra ⋮ Computing branching distances with quantitative games ⋮ Interrupt timed automata: verification and expressiveness ⋮ Discrete-time control for rectangular hybrid automata ⋮ Verification of duration systems using an approximation approach ⋮ Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions ⋮ Automatic verification of reduction techniques in higher order logic ⋮ Efficient verification of distributed real-time systems with broadcasting behaviors ⋮ Improving active Mealy machine learning for protocol conformance testing ⋮ Statistical Verification of Probabilistic Properties with Unbounded Until ⋮ Parameter synthesis for hierarchical concurrent real-time systems ⋮ Analysis of meeting protocols by formalisation, simulation, and verification ⋮ When are timed automata weakly timed bisimilar to time Petri nets? ⋮ The algorithmic analysis of hybrid systems ⋮ Automatic generation of path conditions for concurrent timed systems ⋮ Hybrid automata with finite bisimulations ⋮ The expressive power of clocks ⋮ Automatic synthesis of real time systems ⋮ Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata ⋮ Model checking for probabilistic timed automata ⋮ VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES ⋮ THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Compositional schedulability analysis of real-time actor-based systems ⋮ Detecting synchronisation of biological oscillators by model checking ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ On the expressiveness of TPTL and MTL ⋮ What’s Decidable About Parametric Timed Automata? ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ A contribution to the validation of grafcet controlled systems ⋮ Verifying untimed and timed aspects of the experimental batch plant ⋮ On decidability of recursive weighted logics ⋮ Towards verification of computation orchestration
This page was built for publication: Symbolic model checking for real-time systems
