TY - GEN

T1 - A hemimetric extension of simulation for semi-markov decision processes

AU - Pedersen, Mathias Ruggaard

AU - Bacci, Giorgio

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu

PY - 2018/9/4

Y1 - 2018/9/4

N2 - Semi-Markov decision processes (SMDPs) are continuous-time Markov decision processes where the residence-time on states is governed by generic distributions on the positive real line. In this paper we consider the problem of comparing two SMDPs with respect to their time-dependent behaviour. We propose a hemimetric between processes, which we call simulation distance, measuring the least acceleration factor by which a process needs to speed up its actions in order to behave at least as fast as another process. We show that this distance can be computed in time O(n2(f(l)+k)+mn7), where n is the number of states, m the number of actions, k the number of atomic propositions, and f(l) the complexity of comparing the residence-time between states. The theoretical relevance and applicability of this distance is further argued by showing that (i) it is suitable for compositional reasoning with respect to CSP-like parallel composition and (ii) has a logical characterisation in terms of a simple Markovian logic.

AB - Semi-Markov decision processes (SMDPs) are continuous-time Markov decision processes where the residence-time on states is governed by generic distributions on the positive real line. In this paper we consider the problem of comparing two SMDPs with respect to their time-dependent behaviour. We propose a hemimetric between processes, which we call simulation distance, measuring the least acceleration factor by which a process needs to speed up its actions in order to behave at least as fast as another process. We show that this distance can be computed in time O(n2(f(l)+k)+mn7), where n is the number of states, m the number of actions, k the number of atomic propositions, and f(l) the complexity of comparing the residence-time between states. The theoretical relevance and applicability of this distance is further argued by showing that (i) it is suitable for compositional reasoning with respect to CSP-like parallel composition and (ii) has a logical characterisation in terms of a simple Markovian logic.

KW - semi-Markov decision processes

KW - Markovian logic

UR - http://www.scopus.com/inward/record.url?scp=85053162810&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-99154-2_21

DO - 10.1007/978-3-319-99154-2_21

M3 - Conference contribution book

AN - SCOPUS:85053162810

SN - 9783319991535

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 339

EP - 355

BT - Quantitative Evaluation of Systems - 15th International Conference, QEST 2018, Proceedings

A2 - McIver, Annabelle

A2 - Horvath, Andras

PB - Springer-Verlag

CY - Cham

T2 - 15th International Conference on Quantitative Evaluation of Systems, QEST 2018

Y2 - 4 September 2018 through 7 September 2018

ER -