Model-checking in dense real-time
From MaRDI portal
Publication:689092
DOI10.1006/INCO.1993.1024zbMATH Open0783.68076OpenAlexW1981808971MaRDI QIDQ689092FDOQ689092
Authors: Rajeev Alur, Costas Courcoubetis, David L. Dill 
Publication date: 6 December 1993
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/80a4c1bb7d5c245c9eb9b319e36054af5d6b94f5
Recommendations
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)
Cited In (only showing first 100 items - show all)
- A survey of timed automata for the development of real-time systems
- Model checking weighted integer reset timed automata
- Timed recursive state machines: expressiveness and complexity
- Minimum and maximum delay problems in real-time systems
- PuRSUE -- from specification of robotic environments to synthesis of controllers
- Decision problems for lower/upper bound parametric timed automata
- Scheduling with timed automata
- Interrupt timed automata: verification and expressiveness
- Combined model checking for temporal, probabilistic, and real-time logics
- Timed modal logics for real-time systems. Specification, verification and control
- Efficient timed model checking for discrete-time systems
- On-the-fly \(TCTL\) model checking for time Petri nets
- Tropical Fourier-Motzkin elimination, with an application to real-time verification
- Finite automata on timed \(\omega\)-trees
- Title not available (Why is that?)
- Reachability solution characterization of parametric real-time systems
- Axioms for real-time logics
- Bounded model checking for knowledge and real time
- Event-clock automata: a determinizable class of timed automata
- Adequacy and complete axiomatization for timed modal logic
- Time-abstracted bisimulation: Implicit specifications and decidability
- Verification in loosely synchronous queue-connected discrete timed automata.
- Efficient on-the-fly algorithm for checking alternating timed simulation
- On timed alternating simulation for concurrent timed games
- The algorithmic analysis of hybrid systems
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Title not available (Why is that?)
- Title not available (Why is that?)
- Improved undecidability results on weighted timed automata
- Extending timed automaton and real-time logic to many-valued reasoning
- Model checking temporal properties of reaction systems
- Is your model checker on time? On the complexity of model checking for timed modal logics
- The theory of interactive generalized semi-Markov processes
- Symbolic model checking for real-time systems
- Presburger liveness verification of discrete timed automata.
- A space-efficient on-the-fly algorithm for real-time model checking
- Performance analysis of probabilistic timed automata using digital clocks
- Checking timed Büchi automata emptiness efficiently
- On the optimal reachability problem of weighted timed automata
- Model checking of time Petri nets using the state class timed automaton
- Model checking of biological systems
- Timed CSP = closed timed automata
- Automatic verification of real-time systems with discrete probability distributions.
- How to stop time stopping
- Min-max Computation Tree Logic
- On the expressiveness of TPTL and MTL
- Generalized discrete timed automata: Decidable approximations for safety verification.
- The power of reachability testing for timed automata
- Statistical probabilistic model checking with a focus on time-bounded properties
- Model checking for probabilistic timed automata
- Title not available (Why is that?)
- Parametric metric interval temporal logic
- On regions and zones for event-clock automata
- Symbolic model checking for probabilistic timed automata
- Concavely-Priced Timed Automata
- The automatic verification using symbolic model-checking
- The expressive power of memory logics
- A new model for model checking: cycle-weighted Kripke structure
- On decidability of recursive weighted logics
- Strict Divergence for Probabilistic Timed Automata
- A Graph-Theoretic Approach for Timing Analysis and its Implementation
- Using formal verification to evaluate the execution time of Spark applications
- On Expressiveness and Complexity in Real-Time Model Checking
- Model checking for a class of weighted automata
- Reachability analysis of dynamical systems having piecewise-constant derivatives
- Model-checking precision agriculture logistics: the case of the differential harvest
- Efficient verification of distributed real-time systems with broadcasting behaviors
- Model-checking for real-time systems
- Model checking general linear temporal logic
- On model-checking timed automata with stopwatch observers
- A logical characterization of data languages.
- On the expressivity and complexity of quantitative branching-time temporal logics
- Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
- Branching-time logics with path relativisation
- Automata-theoretic decision of timed games
- Model-checking timed temporal logics
- Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal
- Analysis of equivalence relations of event structures with continuous time
- Dealing with practical limitations of distributed timed model checking for timed automata
- Efficient SAT-based bounded model checking for software verification
- Exact acceleration of real-time model checking
- Spotlight abstraction in model checking real-time task schedulability
- A tableau construction for finite linear-time temporal logic
- Probabilistic timed graph transformation systems
- Formal modeling and analysis of business process timed constraints
- Alternation-free weighted mu-calculus: decidability and completeness
- Title not available (Why is that?)
- Timed games with bounded window parity objectives
- Towards light-weight probabilistic model checking
- Timed CTL model checking in Real-Time Maude
- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
- On reachability and safety in infinite-state systems
- THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS
- revTPL: The Reversible Temporal Process Language
- Timed Petri nets with reset for pipelined synchronous circuit design
- Symbolic and Quantitative Approaches to Reasoning with Uncertainty
- Cancer hybrid automata: model, beliefs and therapy
- Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques
- Parametric real-time model checking using splitting trees
- Verifying distributed real-time properties of embedded systems via graph transformations and model checking
This page was built for publication: Model-checking in dense real-time
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q689092)
