Confluence reduction for Markov automata

Autor: Joost-Pieter Katoen, Mark Timmer, Jaco van de Pol, Mariëlle Stoelinga
Rok vydání: 2016
Předmět:
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES
Theoretical computer science
General Computer Science
Computer science
Process calculus
Markov process
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Theoretical Computer Science
symbols.namesake
Computer Science::Logic in Computer Science
0202 electrical engineering
electronic engineering
information engineering
State space
Markov chain
State space reduction
Probabilistic logic
Process algebra
Confluence
020207 software engineering
Partial order reduction
Automaton
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
symbols
Computer Science::Programming Languages
Markov automata
Divergence-sensitive branching bisimulation
Computer Science::Formal Languages and Automata Theory
Zdroj: Theoretical computer science, 655(B), 193-219. Elsevier
ISSN: 0304-3975
DOI: 10.1016/j.tcs.2016.01.017
Popis: Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. As expected, the state space explosion threatens the analysability of these models. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep them small by omitting internal transitions. We define the notion of confluence directly on Markov automata, and discuss additionally how to syntactically detect confluence on the process-algebraic language MAPA that was introduced recently. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.
Databáze: OpenAIRE
Externí odkaz: