Model-checking in dense real-time
From MaRDI portal
Publication:689092
DOI10.1006/INCO.1993.1024zbMATH Open0783.68076OpenAlexW1981808971MaRDI QIDQ689092FDOQ689092
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
- Efficient SAT-based bounded model checking for software verification
- 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
- Model Checking of Biological Systems
- 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
- Conditional simple temporal networks with uncertainty and decisions
- 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
- 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
- Model-checking Timed Temporal Logics
- 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 Real-Time Systems
- 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
- 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
- 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
- THE EXPRESSIVE POWER OF MEMORY 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
- 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
- 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
- Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
- 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
- Inclusion dynamics hybrid automata
- Timed vacuity
- Wireless ventilation control for large‐scale systems: The mining industrial case
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)
