A Probabilistic Logic for pTiMo

摘要

In this paper we present pTiMo, a process algebra in which migrations and interactions depend upon timers and have probabilities. The semantics of the calculus is given in terms of labeled, discrete-time Markov chains. The existing quantitative tools do not explicitly support properties which make use of local clocks, multisets of transitions (generated by the maximal progress policy in pTiMo) and transition provenance (the location at which a transition originates, and the processes that participate in the transition). In order to study such properties, we introduce a probabilistic temporal logic PLTM for pTiMo, and provide an algorithm for verifying PLTM properties. These properties can be checked over states and/or transitions, and encompass both transient and steady-state behaviors. We also provide a verification algorithm for PLTM properties, and analyze its time complexity.