A Lyapunov Approach for Time Bounded Reachability of CTMCs and CTMDPs
- Submitting institution
-
University of Newcastle upon Tyne
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 262191-227916-1292
- Type
- D - Journal article
- DOI
-
10.1145/3371923
- Title of journal
- ACM Transactions on Modeling and Performance Evaluation of Computing Systems (TOMPECS)
- Article number
- 2
- First page
- -
- Volume
- 5
- Issue
- 1
- ISSN
- 2376-3639
- Open access status
- Compliant
- Month of publication
- February
- Year of publication
- 2020
- URL
-
https://doi.org/10.1145/3371923
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
A - Advanced Model-Based Engineering and Reasoning (AMBER)
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- In this paper we establish that concepts from Control Theory can be used for the verification and synthesis of models traditionally studied in Computer Science. We prove that bisimulation relations are not robust and propose a generalised quantitative relation for probabilistic models using the concept of Lyapunov functions – a major technique in control theory for establishing stability of dynamical systems. This paper won the Best Paper Award from the International Conference on Quantitative Evaluation of Systems (QEST’18), which is the leading forum on quantitative evaluation and verification of computer systems and networks through stochastic models and measurements.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -