Continuous probability and nondeterminism in labeled transaction systems

TitleContinuous probability and nondeterminism in labeled transaction systems
Publication TypeThesis
Year of Publication2012
AuthorsWolovick, N
Academic DepartmentFaMAF
UniversityUniversidad Nacional de Córdoba
Thesis TypePhD
AbstractWe define a model for interacting systems involving continuous probabilistic and nondeterministic choices over continuous state spaces. Our model is a generalization of labeled Markov process, a well established formalism that capture interacting probabilistic continuous systems with strong basis in Measure Theory, but lacking internal nondeterminism. We define the extension to continuous internal nondeterminism in such a way that it allows for quantification of nondeterminism through schedulers, and it also allows for a sound definition of an existential modal operator. The model is used to capture the semantics of a probabilistic timed stochastic process algebra, a stochastic hybrid automata, and a probabilistic and nondeterministic programming language; they are continuous systems involving a nontrivial mix of probabilities and nondeterminism. We also compare our model with other know continuous probabilistic and nondeterministic labeled transition systems and the embedding is defined if applicable. Behavioral equivalence is captured by one notion of point-wise strong bisimulation, and two notions of event-wise strong bisimulation. We show that the three notions are different. We define a two-level infinitary modal logic that characterize the coarser behavioral event-wise bisimulation. Finally we show that a model and a randomized history-dependent scheduler resolving the nondeterminism renders a probabilistic trace semantics.
PDF (Full text): 
Powered by Drupal