Time−Bounded Verification of CTMCs Against Real−Time Specifications

Time−Bounded Verification of CTMCs Against Real−Time Specifications

Abstract. In this paper we study time-bounded verification of a finite continuous-timeMarkov chain (CTMC) C against a real-time specification, provided either as a metric temporal logic (MTL) property 'φ', or as a timed automaton (TA) A. The key question is: what is the probability of the...

Bibliografiset tiedot
Päätekijät:	Chen, T, Diciolla, M, Kwiatkowska, M, Mereacre, A
Aineistotyyppi:	Conference item
Julkaistu:	Springer 2011

Samankaltaisia teoksia

Verification of Linear Duration Properties over Continuous−Time Markov Chains
Tekijä: Chen, T, et al.
Julkaistu: (2012)

Verification of Linear Duration Properties over Continuous Time Markov Chains
Tekijä: Chen, T, et al.
Julkaistu: (2012)

Quantitative Verification of Implantable Cardiac Pacemakers
Tekijä: Chen, T, et al.
Julkaistu: (2015)

A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers
Tekijä: Chen, T, et al.
Julkaistu: (2013)

Synthesising Optimal Timing Delays for Timed I/O Automata
Tekijä: Diciolla, M, et al.
Julkaistu: (2014)

Quantitative verification of real-time properties with application to medical devices
Tekijä: Marco Diciolla, M, et al.
Julkaistu: (2014)

Time-Bounded Verification
Tekijä: Ouaknine, J, et al.
Julkaistu: (2009)

Building power consumption models from executable timed I/O automata specifications
Tekijä: Kwiatkowska, M, et al.
Julkaistu: (2016)

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Tekijä: Taolue Chen, et al.
Julkaistu: (2011-03-01)

PRISM 4.0: Verification of probabilistic real-time systems
Tekijä: Kwiatkowska, M, et al.
Julkaistu: (2011)

Verification and control of turn-based probabilistic real-time games
Tekijä: Kwiatkowska, M, et al.
Julkaistu: (2019)

Real-Time Risk-Bounded Tube-Based Trajectory Safety Verification
Tekijä: Jasour, Ashkan, et al.
Julkaistu: (2022)

Real time programming : languages, specification and verification /
Tekijä: Shyamasundar, Rudrapatna, 1950-, et al.
Julkaistu: (c201)

Real-time systems : formal specification and automatic verification /
Tekijä: 273586, et al.
Julkaistu: (2008)

Towards a Theory of Time-Bounded Verification.
Tekijä: Ouaknine, J, et al.
Julkaistu: (2010)

Real-time face verification
Tekijä: Romano, Raquel Andrea
Julkaistu: (2007)

Efficient CTMC Model Checking of Linear Real−Time Objectives
Tekijä: Barbot, B, et al.
Julkaistu: (2011)

Incremental Verification of Timing Constraints for Real-Time Systems
Tekijä: Andrei, Å tefan, et al.
Julkaistu: (2004)

Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets
Tekijä: QASIM, A., et al.
Julkaistu: (2015-08-01)

Real-time systems : scheduling, analysis, and verification /
Tekijä: 422785 Cheng, Albert M. K.
Julkaistu: (2002)

Modeling and verification of real-time systems /
Tekijä: Navet, Nicolas
Julkaistu: (2008)

Porcine specific real-time polymerase chain reaction (PCR) for halal verification
Tekijä: Khalid, Farihah Liyana, et al.
Julkaistu: (2009)

Time Bounds for Real-time Process Control in the Presence of Time Uncertainty
Tekijä: Attiya, Hagit, et al.
Julkaistu: (2023)

Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata
Tekijä: Kwiatkowska, M, et al.
Julkaistu: (2017)

Formal Verification of Real-Time System Requirements
Tekijä: Marcin Szpyrka
Julkaistu: (2000-01-01)

A lightweight specification language for bounded program verification
Tekijä: Yessenov, Kuat T
Julkaistu: (2010)

Revisiting Timed Specification Theories: A Linear−Time Perspective
Tekijä: Chilton, C, et al.
Julkaistu: (2012)

PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time
Tekijä: Kwiatkowska, M, et al.
Julkaistu: (2020)

Modeling and verification of randomized distributed real-time systems
Tekijä: Segala, Roberto
Julkaistu: (2007)

Modeling and Verification of Randomized Distributed Real -Time Systems
Tekijä: Segala, Roberto
Julkaistu: (2023)

Real-Time Verification for Distributed Cyber-Physical Systems
Tekijä: Tran, Hoang-Dung, et al.
Julkaistu: (2022-12-01)

Time Extensions of Petri Nets for Modelling and Verification of Hard Real-Time Systems
Tekijä: Tomasz Szmuc, et al.
Julkaistu: (2002-01-01)

Formal Verification of Real-Time Function Blocks Using PVS
Tekijä: Linna Pang, et al.
Julkaistu: (2015-06-01)

Linear gate bounds against natural functions for position-verification
Tekijä: Vahid Asadi, et al.
Julkaistu: (2025-01-01)

Specification and Verification of Strong Timing Isolation of Hardware Enclaves
Tekijä: Lau, Stella, et al.
Julkaistu: (2025)

Specification and Verification of Timing Properties in Interoperable Medical Systems
Tekijä: Mahsa Zarneshan, et al.
Julkaistu: (2022-06-01)

Semiautomated Clone Verification by Real-Time PCR Using Molecular Beacons
Tekijä: R.C.A.A. van Schie, et al.
Julkaistu: (2000-12-01)

Verification of audio signal processing algorithm using real-time simulator
Tekijä: Ling, Keck Voon, et al.
Julkaistu: (2013)

Calculation and Verification of the Real-Time Working Characteristics of a Viscous Coupling
Tekijä: Liqiang Jin, et al.
Julkaistu: (2021-01-01)

Event Order Abstraction for Parametric Real-Time System Verification
Tekijä: Umeno, Shinya
Julkaistu: (2008)