Author
|
Conference
|
Journal
|
Organization
|
Year
|
DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all domains
Limit my searches in the following domains
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(9)
Case Study
Discrete Time
Discrete Time Markov Chain
Finite State Automata
Infinite Word
Linear Temporal Logic
Linear Time
Model Checking
Stochastic Hybrid System
Subscribe
Academic
Publications
Quantitative automata model checking of autonomous stochastic hybrid systems
Edit
Quantitative automata model checking of autonomous stochastic hybrid systems
(
Citations: 1
)
BibTex
|
RIS
|
RefWorks
Download
Alessandro Abate
,
Joost-Pieter Katoen
,
Alexandru Mereacre
This paper considers the quantitative verification of discrete-time stochastic hybrid systems (DTSHS) against
linear time
objectives. The central question is to determine the likelihood of all the trajectories in a DTSHS that are accepted by an automaton on finite or infinite words. This verification covers regular and ω-regular properties, and thus comprises the
linear temporal logic
LTL. This work shows that these quantitative verification problems can be reduced to computing reachability probabilities over the product of an automaton and the DTSHS under study. The computation of reachability probabilities can be performed in a backward-recursive manner, and quantitatively approximated by procedures over discrete-time Markov chains. A
case study
shows the feasibility of the approach.
Published in 2011.
DOI:
10.1145/1967701.1967715
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
portal.acm.org
)
(
portal.acm.org
)
Citation Context
(1)
...Theoretically, the connection between the solution of problems related to probabilistic reachability and the verification of PCTL properties has been investigated in [2] and extended to general automata properties in [
3
]...
...In the end, this technique allows to express classes of probabilistic specifications [
3
], [4] over SHS and to compute...
Sadegh Esmaeil Zadeh Soudjani
,
et al.
Adaptive Gridding for Abstraction and Verification of Stochastic Hybri...
References
(15)
Principles of model checking
(
Citations: 178
)
Christel Baier
,
Joost-Pieter Katoen
Published in 2008.
Reachability Questions in Piecewise Deterministic Markov Processes
(
Citations: 44
)
Manuela L. Bujorianu
,
John Lygeros
Conference:
Hybrid Systems
, pp. 126-140, 2003
To the editors
(
Citations: 114
)
J Lowder
,
M. B. Henry Devine
,
Douglas MoRae
Journal:
Clinical Microbiology Newsletter
, vol. 16, no. 24, pp. 191-192, 1994
Computable CTL* for Discrete-Time and Continuous-Space Dynamic Systems
(
Citations: 2
)
Pieter Collins
,
Ivan S. Zapreev
Conference:
Conference on Computability in Europe - CIE
, pp. 107-119, 2009
An Optimal Automata Approach to LTL Model Checking of Probabilistic Systems
(
Citations: 20
)
Jean-michel Couvreur
,
Nasser Saheb
,
Grégoire Sutre
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming - LPAR(RCLP)
, pp. 361-375, 2003
Order by:
Citations
(1)
Adaptive Gridding for Abstraction and Verification of Stochastic Hybrid Systems
Sadegh Esmaeil Zadeh Soudjani
,
Alessandro Abate
Conference:
Quantitative Evaluation of Systems - QEST
, 2011