Analyzing Non-Markovian Systems by Using a Stochastic Process Calculus and a Probabilistic Model Checker

Gabriel Ciobanu ()
Additional contact information
Gabriel Ciobanu: Faculty of Computer Science, Alexandru Ioan Cuza University, 700506 Iaşi, Romania

Mathematics, 2023, vol. 11, issue 2, 1-17

Abstract: The non-Markovian systems represent almost all stochastic processes, except of a small class having the Markov property; it is a real challenge to analyze these systems. In this article, we present a general method of analyzing non-Markovian systems. The novel viewpoint is given by the use of a compact stochastic process calculus developed in the formal framework of computer science for describing concurrent systems. Since phase-type distributions can approximate non-Markovian systems with arbitrary precision, we approximate a non-Markovian system by describing it easily in our stochastic process calculus, which employs phase-type distributions. The obtained process (in our calculus) are then translated into the probabilistic model checker PRISM; by using this free software tool, we can analyze several quantitative properties of the Markovian approximation of the initial non-Markovian system.

Keywords: process calculus; phase-type distribution; non-Markovian systems; model checker PRISM (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2023
References: View references in EconPapers View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/11/2/302/pdf (application/pdf)
https://www.mdpi.com/2227-7390/11/2/302/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:11:y:2023:i:2:p:302-:d:1027669

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().