Model-checking in dense real-time
From MaRDI portal
Publication:689092
DOI10.1006/inco.1993.1024zbMath0783.68076OpenAlexW1981808971MaRDI QIDQ689092
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
Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (only showing first 100 items - show all)
Timed recursive state machines: expressiveness and complexity ⋮ 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 ⋮ Efficient scaling-invariant checking of timed bisimulation ⋮ Symbolic model checking for probabilistic timed automata ⋮ Modeling for Verification ⋮ Model Checking Real-Time Systems ⋮ Improved undecidability results on weighted timed automata ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ On the optimal reachability problem of weighted timed automata ⋮ Verifying distributed real-time properties of embedded systems via graph transformations and model checking ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ How to stop time stopping ⋮ 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 ⋮ Reachability analysis of dynamical systems having piecewise-constant derivatives ⋮ A new model for model checking: cycle-weighted Kripke structure ⋮ Polynomial interrupt timed automata: verification and expressiveness ⋮ A tableau construction for finite linear-time temporal logic ⋮ Branching-time logics with path relativisation ⋮ Automata-theoretic decision of timed games ⋮ A survey of timed automata for the development of real-time systems ⋮ Finite automata on timed \(\omega\)-trees ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ The power of reachability testing for timed automata ⋮ Model checking computation tree logic over finite lattices ⋮ Verification in loosely synchronous queue-connected discrete timed automata. ⋮ Generalized discrete timed automata: Decidable approximations for safety verification. ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ Pushdown timed automata: A binary reachability characterization and safety verification. ⋮ PuRSUE -- from specification of robotic environments to synthesis of controllers ⋮ Dealing with practical limitations of distributed timed model checking for timed automata ⋮ Superposition as a decision procedure for timed automata ⋮ Interrupt timed automata: verification and expressiveness ⋮ Model-checking precision agriculture logistics: the case of the differential harvest ⋮ Efficient verification of distributed real-time systems with broadcasting behaviors ⋮ Concavely-Priced Timed Automata ⋮ Cancer hybrid automata: model, beliefs and therapy ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ Parametric metric interval temporal logic ⋮ On regions and zones for event-clock automata ⋮ Expressiveness of verifiable hierarchical clock systems ⋮ The algorithmic analysis of hybrid systems ⋮ Efficient SAT-based bounded model checking for software verification ⋮ Model checking temporal properties of reaction systems ⋮ Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata ⋮ Model checking for probabilistic timed automata ⋮ Probabilistic timed graph transformation systems ⋮ INDUCTIVE COMPOSITION OF NUMBERS WITH MAXIMUM, MINIMUM, AND ADDITION: A New Theory for Program Execution-Time Analysis ⋮ VERIFICATION IN QUEUE-CONNECTED MULTICOUNTER MACHINES ⋮ THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS ⋮ Unnamed Item ⋮ Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties ⋮ Model checking weighted integer reset timed automata ⋮ Monotonic hybrid systems ⋮ A menagerie of timed automata ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Reachability solution characterization of parametric real-time systems ⋮ On model-checking timed automata with stopwatch observers ⋮ On the expressiveness of TPTL and MTL ⋮ On timed alternating simulation for concurrent timed games ⋮ Unnamed Item ⋮ Timed vacuity ⋮ Model checking restricted sets of timed paths ⋮ Statistical probabilistic model checking with a focus on time-bounded properties ⋮ Inclusion dynamics hybrid automata ⋮ On-the-fly \(TCTL\) model checking for time Petri nets ⋮ On decidability of recursive weighted logics ⋮ THE EXPRESSIVE POWER OF MEMORY LOGICS ⋮ Event-clock automata: a determinizable class of timed automata ⋮ Wireless ventilation control for large‐scale systems: The mining industrial case ⋮ Model-checking Timed Temporal Logics ⋮ Bounded model checking for knowledge and real time ⋮ Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis ⋮ Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation ⋮ On Improving Backwards Verification of Timed Automata (Extended Abstract) ⋮ Exact Acceleration of Real-Time Model Checking ⋮ Timed Semantics of Message Sequence Charts Based on Timed Automata ⋮ Parking Can Get You There Faster ⋮ Timed CSP = Closed Timed Automata1 ⋮ Decision problems for lower/upper bound parametric timed automata ⋮ Using formal verification to evaluate the execution time of Spark applications ⋮ Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal ⋮ Conditional simple temporal networks with uncertainty and decisions ⋮ Min-max event-triggered computation tree logic ⋮ Towards light-weight probabilistic model checking ⋮ Analysis of equivalence relations of event structures with continuous time ⋮ A logical characterization of data languages. ⋮ Parametric multisingular hybrid Petri nets: formal definitions and analysis techniques ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Automated formal analysis and verification: an overview ⋮ The theory of interactive generalized semi-Markov processes ⋮ Automatic verification of real-time systems with discrete probability distributions. ⋮ Timed games with bounded window parity objectives ⋮ Timed Petri nets with reset for pipelined synchronous circuit design ⋮ Checking timed Büchi automata emptiness efficiently
This page was built for publication: Model-checking in dense real-time
