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...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí:	Chen, T, Diciolla, M, Kwiatkowska, M, Mereacre, A
Formáid:	Conference item
Foilsithe / Cruthaithe:	Springer 2011

Míreanna comhchosúla

Verification of Linear Duration Properties over Continuous−Time Markov Chains
de réir: Chen, T, et al.
Foilsithe / Cruthaithe: (2012)

Verification of Linear Duration Properties over Continuous Time Markov Chains
de réir: Chen, T, et al.
Foilsithe / Cruthaithe: (2012)

Quantitative Verification of Implantable Cardiac Pacemakers
de réir: Chen, T, et al.
Foilsithe / Cruthaithe: (2015)

A Simulink Hybrid Heart Model for Quantitative Verification of Cardiac Pacemakers
de réir: Chen, T, et al.
Foilsithe / Cruthaithe: (2013)

Synthesising Optimal Timing Delays for Timed I/O Automata
de réir: Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Quantitative verification of real-time properties with application to medical devices
de réir: Marco Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Time-Bounded Verification
de réir: Ouaknine, J, et al.
Foilsithe / Cruthaithe: (2009)

Building power consumption models from executable timed I/O automata specifications
de réir: Kwiatkowska, M, et al.
Foilsithe / Cruthaithe: (2016)

Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
de réir: Taolue Chen, et al.
Foilsithe / Cruthaithe: (2011-03-01)

PRISM 4.0: Verification of probabilistic real-time systems
de réir: Kwiatkowska, M, et al.
Foilsithe / Cruthaithe: (2011)

Verification and control of turn-based probabilistic real-time games
de réir: Kwiatkowska, M, et al.
Foilsithe / Cruthaithe: (2019)

Real-Time Risk-Bounded Tube-Based Trajectory Safety Verification
de réir: Jasour, Ashkan, et al.
Foilsithe / Cruthaithe: (2022)

Real time programming : languages, specification and verification /
de réir: Shyamasundar, Rudrapatna, 1950-, et al.
Foilsithe / Cruthaithe: (c201)

Real-time systems : formal specification and automatic verification /
de réir: 273586, et al.
Foilsithe / Cruthaithe: (2008)

Towards a Theory of Time-Bounded Verification.
de réir: Ouaknine, J, et al.
Foilsithe / Cruthaithe: (2010)

Real-time face verification
de réir: Romano, Raquel Andrea
Foilsithe / Cruthaithe: (2007)

Efficient CTMC Model Checking of Linear Real−Time Objectives
de réir: Barbot, B, et al.
Foilsithe / Cruthaithe: (2011)

Incremental Verification of Timing Constraints for Real-Time Systems
de réir: Andrei, Å tefan, et al.
Foilsithe / Cruthaithe: (2004)

Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets
de réir: QASIM, A., et al.
Foilsithe / Cruthaithe: (2015-08-01)

Real-time systems : scheduling, analysis, and verification /
de réir: 422785 Cheng, Albert M. K.
Foilsithe / Cruthaithe: (2002)

Modeling and verification of real-time systems /
de réir: Navet, Nicolas
Foilsithe / Cruthaithe: (2008)

Porcine specific real-time polymerase chain reaction (PCR) for halal verification
de réir: Khalid, Farihah Liyana, et al.
Foilsithe / Cruthaithe: (2009)

Time Bounds for Real-time Process Control in the Presence of Time Uncertainty
de réir: Attiya, Hagit, et al.
Foilsithe / Cruthaithe: (2023)

Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata
de réir: Kwiatkowska, M, et al.
Foilsithe / Cruthaithe: (2017)

Formal Verification of Real-Time System Requirements
de réir: Marcin Szpyrka
Foilsithe / Cruthaithe: (2000-01-01)

A lightweight specification language for bounded program verification
de réir: Yessenov, Kuat T
Foilsithe / Cruthaithe: (2010)

Revisiting Timed Specification Theories: A Linear−Time Perspective
de réir: Chilton, C, et al.
Foilsithe / Cruthaithe: (2012)

PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time
de réir: Kwiatkowska, M, et al.
Foilsithe / Cruthaithe: (2020)

Modeling and verification of randomized distributed real-time systems
de réir: Segala, Roberto
Foilsithe / Cruthaithe: (2007)

Modeling and Verification of Randomized Distributed Real -Time Systems
de réir: Segala, Roberto
Foilsithe / Cruthaithe: (2023)

Real-Time Verification for Distributed Cyber-Physical Systems
de réir: Tran, Hoang-Dung, et al.
Foilsithe / Cruthaithe: (2022-12-01)

Time Extensions of Petri Nets for Modelling and Verification of Hard Real-Time Systems
de réir: Tomasz Szmuc, et al.
Foilsithe / Cruthaithe: (2002-01-01)

Formal Verification of Real-Time Function Blocks Using PVS
de réir: Linna Pang, et al.
Foilsithe / Cruthaithe: (2015-06-01)

Linear gate bounds against natural functions for position-verification
de réir: Vahid Asadi, et al.
Foilsithe / Cruthaithe: (2025-01-01)

Specification and Verification of Strong Timing Isolation of Hardware Enclaves
de réir: Lau, Stella, et al.
Foilsithe / Cruthaithe: (2025)

Specification and Verification of Timing Properties in Interoperable Medical Systems
de réir: Mahsa Zarneshan, et al.
Foilsithe / Cruthaithe: (2022-06-01)

Semiautomated Clone Verification by Real-Time PCR Using Molecular Beacons
de réir: R.C.A.A. van Schie, et al.
Foilsithe / Cruthaithe: (2000-12-01)

Verification of audio signal processing algorithm using real-time simulator
de réir: Ling, Keck Voon, et al.
Foilsithe / Cruthaithe: (2013)

Calculation and Verification of the Real-Time Working Characteristics of a Viscous Coupling
de réir: Liqiang Jin, et al.
Foilsithe / Cruthaithe: (2021-01-01)

Event Order Abstraction for Parametric Real-Time System Verification
de réir: Umeno, Shinya
Foilsithe / Cruthaithe: (2008)