scientific article; zbMATH DE number 176728

zbMATH Open0769.68088MaRDI QIDQ4036557FDOQ4036557

Authors: Rajeev Alur, Costas Courcoubetis, David L. Dill 

Publication date: 18 May 1993

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 1507207
• Model checking of probabilistic and nondeterministic systems
• Model checking stochastic automata
• Symbolic model checking for real-time systems
• Model checking probabilistic systems

zbMATH Keywords

model-checkingverification of concurrent systemsbranching-time temporal logicgeneralized semi-Markov processesfinite-state discrete-time Markov chainsstochastic real-time systems

Mathematics Subject Classification ID

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

Cited In (only showing first 100 items - show all)

• A survey of timed automata for the development of real-time systems
• Deciding properties of integral relational automata
• Foundations of Software Science and Computational Structures
• Probabilistic and Topological Semantics for Timed Automata
• On impulsive boundary value problems of fractional differential equations with irregular boundary conditions
• Stochastic model checking of the stochastic quality calculus
• Modular abstractions for verifying real-time distributed systems
• Specification and automatic verification of self-timed queues
• Exact acceleration of real-time model checking
• Minimum and maximum delay problems in real-time systems
• Undecidable verification problems for programs with unreliable channels
• Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions
• The well-designed logical robot: learning and experience from observations to the Situation Calculus
• Efficient timed model checking for discrete-time systems
• Model-checking in dense real-time
• Symbolic model checking for probabilistic processes
• Automatic synthesis of real time systems
• A theory of timed automata
• Verifying automata specification of distributed probabilistic real-time systems
• Temporal specifications with accumulative values
• Language emptiness of continuous-time parametric timed automata
• Model checking probabilistic systems
• Stochastic model checking
• Model checking probabilistic real-time properties for service-oriented systems with service level agreements
• Uniformity for the decidability of hybrid automata
• Accuracy of message counting abstraction in fault-tolerant distributed algorithms
• Information system design of manufacturing environments
• VERICS 2007 -- a model checker for knowledgee and real-time
• Using mappings to prove timing properties
• Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}
• A logic for reasoning about time and reliability
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• Algebraic Methodology and Software Technology
• Symbolic model checking for real-time systems
• Duration calculus: Logical foundations
• A supervisory control method for ensuring the conformance of real-time discrete event systems
• Checking timed Büchi automata emptiness efficiently
• Verifying temporal properties in real models
• Temporal logics for the specification of performance and reliability
• A theory of stochastic systems. I: Stochastic automata
• Automatic verification of real-time systems with discrete probability distributions.
• Network invariants for real-time systems
• Ensuring completeness of symbolic verification methods for infinite-state systems
• On the expressiveness of TPTL and MTL
• PLC-automata: A new class of implementable real-time automata
• On Caputo-Hadamard type fractional impulsive hybrid systems with nonlinear fractional integral conditions
• Time-Bounded Verification
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Title not available (Why is that?)
• Correct Hardware Design and Verification Methods
• Statistical probabilistic model checking with a focus on time-bounded properties
• Model Checking Real-Time Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• From ATP to timed graphs and hybrid systems
• Local model checking and protocol analysis
• Extending CTL with Actions and Real Time
• Verification of continuous dynamical systems by timed automata
• Model checking for probabilistic timed automata
• Title not available (Why is that?)
• Model Checking HML on Piecewise-Constant Inhomogeneous Markov Chains
• A new model for model checking: cycle-weighted Kripke structure
• Formal Modeling and Analysis of Timed Systems
• A note on the attractor-property of infinite-state Markov chains
• Strict Divergence for Probabilistic Timed Automata
• Model checking of probabilistic and nondeterministic systems
• Model Checking Temporal Metric Specifications with Trio2Promela
• Model-checking discrete duration calculus
• Model checking of systems with many identical timed processes
• An iterative approach to verification of real-time systems
• Model-checking for real-time systems
• Validation of Stochastic Systems
• Title not available (Why is that?)
• On the expressivity and complexity of quantitative branching-time temporal logics
• Formal Techniques for Networked and Distributed Systems - FORTE 2005
• Model Checking Software
• Model-checking timed temporal logics
• Monitoring Temporal Properties of Stochastic Systems
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Title not available (Why is that?)
• Model checking functional and performability properties of stochastic fluid models
• Cyber-physical systems
• Comparing model checking and logical reasoning for real-time systems
• A maximal entropy stochastic process for a timed automaton
• Verification of duration systems using an approximation approach
• Performance evaluation of schedulers in a probabilistic setting
• On a class of timer hybrid systems reducible to finite state automata
• Games, Time, and Probability: Graph Models for System Design and Analysis
• Model checking real-time systems within unified approach of timed interval temporal logic
• Symbolic Branching Bisimulation-Checking of Dense-Time Systems in an Environment
• Title not available (Why is that?)
• Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
• Faster SPDL Model Checking Through Property-Driven State Space Generation
• Fixed-delay events in generalized semi-Markov processes revisited
• Probabilistic temporal logics via the modal mu-calculus
• On-the-fly model checking for extended action-based probabilistic operators
• Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras
• TPAP: an algebra of preemptive processes for verifying real-time systems with shared resources
• Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format
• Title not available (Why is that?)
• Finite horizon analysis of stochastic systems with the Mur\(\varphi \) verifier.

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4036557)