Time-Bounded Verification of CTMCs against Real-Time Specifications

No abstract is available for this paper.

• Publication year

  2011

• Venue

  International Conference on Formal Modeling and Analysis of Timed Systems

• Publication date

  2011-09-21

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/978-3-642-24310-3_4
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications

  2011cited by this paper
• Weighted Lumpability on Markov Chains

  2011cited by this paper
• Wiley‐Interscience Series in Discrete Mathematics and Optimization

  2011cited by this paper
• Efficient CTMC Model Checking of Linear Real-Time Objectives

  2011influential reference
• Being Van Kampen is a universal property

  2011cited by this paper
• Performance evaluation and model checking join forces

  2010cited by this paper
• From Mtl to Deterministic Timed Automata

  2010cited by this paper
• Alternating Timed Automata over Bounded Time

  2010cited by this paper
• Towards a Theory of Time-Bounded Verification

  2010cited by this paper
• Model Checking Timed and Stochastic Properties with CSL^{TA}

  2009cited by this paper
• Time-Bounded Verification

  2009cited by this paper
• From Qualitative to Quantitative Analysis of Timed Systems

  2009cited by this paper
• CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings

  2009cited by this paper
• Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets

  2008cited by this paper
• Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

  2008cited by this paper
• Model Checking Markov Chains with Actions and State Labels

  2007influential reference
• On the decidability and complexity of Metric Temporal Logic over finite words

  2007cited by this paper
• Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes

  2005cited by this paper
• On the Expressiveness of TPTL and MTL

  2005cited by this paper
• Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability

  2005cited by this paper
• A Temporal Logic of Nested Calls and Returns

  2004cited by this paper
• Model-Checking Algorithms for Continuous-Time Markov Chains

  2002influential reference
• Convexity recognition of the union of polyhedra

  2001cited by this paper
• A Laplace transform algorithm for the volume of a convex polytope

  2001cited by this paper
• Model Checking of Safety Properties

  1999influential reference
• Membership questions for timed and hybrid automata

  1998cited by this paper
• Complexity and Real Computation

  1997cited by this paper
• The complexity of probabilistic verification

  1995cited by this paper
• Verifying Time-bounded Properties for ELECTRE Reactive Programs with Stopwatch Automata

  1994cited by this paper
• A Theory of Timed Automata

  1994cited by this paper
• Hybrid Systems II

  1994cited by this paper
• Convex analysis and minimization algorithms

  1993cited by this paper
• The benefits of relaxing punctuality

  1991cited by this paper
• Specifying real-time properties with metric temporal logic

  1990cited by this paper
• Real-time logics: complexity and expressiveness

  1990cited by this paper
• REAL-TIME SYSTEMS .2.

  1989cited by this paper
• A really temporal logic

  1989cited by this paper
• THEORY OF LINEAR AND INTEGER PROGRAMMING (Wiley-Interscience Series in Discrete Mathematics and Optimization)

  1989cited by this paper
• Theory of linear and integer programming

  1986cited by this paper
• An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)

  1986cited by this paper
• Automatic verification of probabilistic concurrent finite state programs

  1985cited by this paper
• On Observing Nondeterminism and Concurrency

  1980cited by this paper
• Functions of a Complex Variable

  1957cited by this paper

• Combining Quantitative Data with Logic-Based Specifications for Parameter Inference

  2021cites this paper
• Quantitative Evaluation of Systems: 17th International Conference, QEST 2020, Vienna, Austria, August 31 – September 3, 2020, Proceedings

  2020cites this paper
• A Probabilistic Logic for Verifying Continuous-time Markov Chains

  2020influential citation
• Bounding Mean First Passage Times in Population Continuous-Time Markov Chains

  2019cites this paper
• The Linear Time-Branching Time Spectrum of Equivalences for Stochastic Systems with Non-determinism

  2019cites this paper
• BAYESIAN STATISTICAL PARAMETRIC VERIFICATION AND SYNTHESIS BY MACHINE LEARNING

  2018cites this paper
• BAYESIAN STATISTICAL PARAMETRIC VERIFICATION AND SYNTHESIS BY MACHINE LEARNING

  2018cites this paper
• On the limits of information spread by memory-less agents

  2018cites this paper
• Monitoring CTMCs by Multi-clock Timed Automata

  2018cites this paper
• ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains

  2017cites this paper
• When are Stochastic Transition Systems Tameable?

  2017cites this paper
• Safety Verification of Continuous-Space Pure Jump Markov Processes

  2016cites this paper
• On the Total Variation Distance of Semi-Markov Chains

  2015cites this paper
• On Quantitative Modelling and Verification of DNA Walker Circuits Using Stochastic Petri Nets

  2015cites this paper
• Application and Theory of Petri Nets and Concurrency

  2015cites this paper
• HASL: A new approach for performance evaluation and model checking from concepts to experimentation

  2015cites this paper
• Machine Learning Methods in Statistical Model Checking and System Design - Tutorial

  2015cites this paper
• System design of stochastic models using robustness of temporal properties

  2015cites this paper
• Model checking single agent behaviours by fluid approximation

  2015cites this paper
• Learning and Designing Stochastic Processes from Logical Constraints

  2015influential citation
• Foundations of Software Science and Computation Structures

  2015influential citation
• Topologies of Stochastic Markov Models: Computational Aspects

  2014cites this paper
• Smoothed model checking for uncertain Continuous-Time Markov Chains

  2014cites this paper
• Data-Driven Statistical Learning of Temporal Logic Properties

  2014cites this paper
• Verification of linear duration properties over continuous-time markov chains

  2013cites this paper
• Model checking conditional CSL for continuous-time Markov chains

  2013cites this paper
• Verification of Linear Duration Properties over Continuous Time

  2013cites this paper
• From software verification to ‘everyware’ verification

  2013cites this paper
• Learning and Designing Stochastic Processes from Logical Constraints

  2013influential citation
• On the Robustness of Temporal Properties for Stochastic Models

  2013cites this paper
• Fluid Model Checking

  2012cites this paper
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata

  2012cites this paper
• Bisimulations and Logical Characterizations on Continuous-Time Markov Decision Processes

  2012cites this paper
• Verification of linear duration properties over continuous-time markov chains

  2012cites this paper