2012 | OriginalPaper | Buchkapitel
Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation
verfasst von : Pedro Rubén D’Argenio, Matias David Lee
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present a format for the specification of probabilistic transition systems that guarantees that bisimulation equivalence is a congruence for any operator defined in this format. In this sense, the format is somehow comparable to the
ntyft/ntyxt
format in a non-probabilistic setting. We also study the modular construction of probabilistic transition systems specifications and prove that some standard conservative extension theorems also hold in our setting. Finally, we show that the trace congruence for image-finite processes induced by our format is precisely bisimulation on probabilistic systems.