scientific article

Rajeev Alur, David L. Dill, Costas Courcoubetis

Publication date: 18 May 1993

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

model-checking verification of concurrent systems branching-time temporal logic generalized semi-Markov processes finite-state discrete-time Markov chains stochastic real-time systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (65)

Efficient timed model checking for discrete-time systems ⋮ Language Emptiness of Continuous-Time Parametric Timed Automata ⋮ Performance Evaluation of Schedulers in a Probabilistic Setting ⋮ A logic for reasoning about time and reliability ⋮ An iterative approach to verification of real-time systems ⋮ Model-checking discrete duration calculus ⋮ Model-checking for real-time systems ⋮ Time-Bounded Verification ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ A calculus of stochastic systems for the specification, simulation, and hidden state estimation of mixed stochastic/nonstochastic systems ⋮ A new model for model checking: cycle-weighted Kripke structure ⋮ Symbolic model checking for probabilistic processes ⋮ Duration calculus: Logical foundations ⋮ Temporal Specifications with Accumulative Values ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ A survey of timed automata for the development of real-time systems ⋮ On the expressivity and complexity of quantitative branching-time temporal logics ⋮ On Caputo-Hadamard type fractional impulsive hybrid systems with nonlinear fractional integral conditions ⋮ Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms ⋮ Cyber-physical systems ⋮ Superposition as a decision procedure for timed automata ⋮ Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL} ⋮ Verification of duration systems using an approximation approach ⋮ Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions ⋮ Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains ⋮ Deciding properties of integral relational automata ⋮ Automatic synthesis of real time systems ⋮ Modular abstractions for verifying real-time distributed systems ⋮ Minimum and maximum delay problems in real-time systems ⋮ Specification and automatic verification of self-timed queues ⋮ Model checking for probabilistic timed automata ⋮ Bayesian statistical model checking with application to Stateflow/Simulink verification ⋮ Using mappings to prove timing properties ⋮ On impulsive boundary value problems of fractional differential equations with irregular boundary conditions ⋮ The well-designed logical robot: learning and experience from observations to the Situation Calculus ⋮ A menagerie of timed automata ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ On the expressiveness of TPTL and MTL ⋮ Statistical probabilistic model checking with a focus on time-bounded properties ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Probabilistic and Topological Semantics for Timed Automata ⋮ Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment ⋮ Fixed-Delay Events in Generalized Semi-Markov Processes Revisited ⋮ Verifying automata specification of distributed probabilistic real-time systems ⋮ Model-checking Timed Temporal Logics ⋮ Verification of continuous dynamical systems by timed automata ⋮ Information system design of manufacturing environments ⋮ TPAP ⋮ Probabilistic temporal logics via the modal mu-calculus ⋮ A note on the attractor-property of infinite-state Markov chains ⋮ On a class of timer hybrid systems reducible to finite state automata ⋮ PLC-automata: A new class of implementable real-time automata ⋮ A theory of stochastic systems. I: Stochastic automata ⋮ Model checking of systems with many identical timed processes ⋮ Calculating Probabilities of Real-Time Test Cases ⋮ On the verification of qualitative properties of probabilistic processes under fairness constraints. ⋮ A maximal entropy stochastic process for a timed automaton ⋮ Automatic verification of real-time systems with discrete probability distributions. ⋮ Undecidable verification problems for programs with unreliable channels ⋮ Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras ⋮ A theory of timed automata ⋮ From ATP to timed graphs and hybrid systems ⋮ Checking timed Büchi automata emptiness efficiently ⋮ A supervisory control method for ensuring the conformance of real-time discrete event systems ⋮ Uniformity for the decidability of hybrid automata

This page was built for publication: