Bisimulations, logics, and trace distributions for stochastic systems with rewards
Pages 31 - 40
Abstract
Stochastic systems with rewards yield a generic stochastic model where both the state and the action space might be uncountable and where every action is decorated by a real-valued reward. For every deterministic stochastic system with rewards we prove that the bisimulation relation and the trace-distribution relation collapse. As a second result, we also establish a characterisation of the bisimulation relation in terms of an expressive action-based probabilistic logic and show that this characterisation is still maintained by a small fragment of this logic.
References
[1]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. 2010. Approximate model checking of stochastic hybrid systems. European Journal of Control 16, 6 (2010), 624--641.
[2]
Alessandro Abate, Joost-Pieter Katoen, and Alexandru Mereacre. 2011. Quantitative automata model checking of autonomous stochastic hybrid systems. In 14th International Conference on Hybrid Systems: Computation and Control (HSCC). ACM, 83--92.
[3]
Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126 (1994), 183--235.
[4]
Adnan Aziz, Kumud Sanwal, Vigyan Singhal, and Robert Brayton. 2000. Verifying continuous time Markov chains. ACM Transactions on Computational Logic 1, 1 (2000), 162--170.
[5]
Adnan Aziz, Vigyan Singhal, Felice Balarin, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. 1995. It usually works: the temporal logic of stochastic systems. In 7th International Conference on Computer Aided Verification (CAV). Springer, 155--165.
[6]
Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2000. On the logical characterisation of performability properties. In 27th International Colloquium on Automata, Languages and Programming (ICALP). Springer, 780--792.
[7]
Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen. 2003. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29, 7 (2003).
[8]
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.
[9]
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. 2005. Comparative branching-time semantics for Markov chains. Information and Computation 200, 2 (2005), 149--214.
[10]
Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich. 2014. Weight monitoring with linear temporal logic: complexity and decidability. In Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, Article 11, 10 pages.
[11]
Mikhail Bernadsky, Raman Sharykin, and Rajeev Alur. 2004. Structured modeling of concurrent stochastic hybrid systems. In Joint International Conferences on Formal Modeling and Analysis of Timed Systems (FORMATS) and on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT). Springer, 309--324.
[12]
Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdziński. 2014. Stochastic timed automata. Logical Methods in Computer Science 10, 4:6 (2014).
[13]
Gaoang Bian and Alessandro Abate. 2017. On the relationship between bisimulation and trace equivalence in an approximate probabilistic context. In 20th International Conference on Foundations of Software Science and Computational Structures (FOSSACS) (Lecture Notes in Computer Science). Springer, 321--337.
[14]
Andrea Bianco and Luca de Alfaro. 1995. Model checking of probabilistic and nondeterministic systems. In 15th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS). Springer, 499--513.
[15]
Vladimir Igorevich Bogachev. 2007. Measure theory. Vol. 1 and 2. Springer.
[16]
Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. 2014. Temporal specifications with accumulative values. ACM Transactions on Computational Logic 15, 4, Article 27 (2014), 25 pages.
[17]
Patricia Bouyer, Thomas Brihaye, Pierre Carlier, and Quentin Menet. 2016. Compositional design of stochastic timed automata. In 11th International Computer Science Symposium in Russia (CSR) (Lecture Notes in Computer Science). Springer, 117--130.
[18]
Manuela L. Bujorianu, John Lygeros, and Marius C. Bujorianu. 2005. Bisimulation for general stochastic hybrid systems. In 8th International Conference on Hybrid Systems: Computation and Control (HSCC). Springer, 198--214.
[19]
Stefano Cattani. 2005. Trace-based process algebras for real-time probabilistic systems. Ph.D. Dissertation. University of Birmingham.
[20]
Stefano Cattani, Roberto Segala, Marta Z. Kwiatkowska, and Gethin Norman. 2005. Stochastic transition systems for continuous state spaces and non-determinism. In 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS) (Lecture Notes in Computer Science), Vol. 3441. Springer, 125--139.
[21]
Pedro R. D'Argenio. 1999. Algebras and automata for timed and stochastic systems. Ph.D. Dissertation. University of Twente.
[22]
Pedro R. D'Argenio and Joost-Pieter Katoen. 2005. A theory of stochastic systems part I: stochastic automata and part II: process algebra. Information and Computation 203, 1 (2005), 1--74.
[23]
Pedro R. D'Argenio, Pedro Sánchez Terraf, and Nicolás Wolovick. 2012. Bisimulations for non-deterministic labelled Markov processes. Mathematical Structures in Computer Science 22 (2012), 43--68. Issue 01.
[24]
M. H. A. Davis. 1984. Piecewise-deterministic Markov processes: a general class of nondiffusion stochastic models. Journal of the Royal Statistical Society Series B 46, 3 (1984), 353--388.
[25]
Rocco De Nicola and Frits Vaandrager. 1990. Action versus state based logics for transition systems. In LITP Spring School on Theoretical Computer Science La Roche Posay (Semantics of Systems of Concurrent Processes). Springer, 407--419.
[26]
Yuxin Deng. 2014. Semantics of probabilistic processes: an operational approach. Springer-Verlag and Shanghai Jiao Tong University Press.
[27]
Yuxin Deng and Matthew Hennessy. 2013. On the semantics of Markov automata. Information and Computation 222 (2013), 139--168.
[28]
Josée Desharnais, Abbas Edalat, and Prakash Panangaden. 2002. Bisimulation for labelled Markov processes. Information and Computation 179, 2 (2002), 163--193.
[29]
Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. 2003. Approximating labelled Markov processes. Information and Computation 184, 1 (2003), 160--200.
[30]
Josée Desharnais, Francois Laviolette, and Mathieu Tracol. 2008. Approximate analysis of probabilistic processes: logic, simulation and games. In 5th International Conference on Quantitative Evaluation of Systems (QEST). 264--273.
[31]
Josée Desharnais and Prakash Panangaden. 2003. Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes. The Journal of Logic and Algebraic Programming 56, 1 (2003), 99--115.
[32]
Ernst-Erich Doberkat. 2007. Stochastic relations: foundations for Markov transition systems. CRC Press. https://books.google.pl/books?id=_OmI_xrYqawC
[33]
Christian Eisentraut, Holger Hermanns, and Lijun Zhang. 2010. On probabilistic automata in continuous time. In 25th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 342--351.
[34]
E. Allen Emerson and Edmund M. Clarke. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2, 3 (1982), 241--266.
[35]
Sadegh Esmaeil Zadeh Soudjani, Rupak Majumdar, and Alessandro Abate. 2016. Safety verification of continuous-space pure jump Markov processes. In 22nd Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 147--163.
[36]
Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. 2017. Expressiveness of probabilistic modal logics, revisited. In 44th International Colloquium on Automata, Languages and Programming (ICALP) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 80. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 105:1--105:12.
[37]
Daniel Gburek and Christel Baier. 2017. Stochastic transition systems: composition operators, simulations, and trace distributions. (2017). Submitted.
[38]
Daniel Gburek, Christel Baier, and Sascha Klüppelholz. 2016. Composition of stochastic transition systems based on spans and couplings. In 43rd International Colloquium on Automata, Languages and Programming (ICALP) (Leibniz International Proceedings in Informatics (LIPIcs)), Vol. 55. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 102:1--102:15. extended version available at https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ICALP16/.
[39]
Rob J. van Glabbeek, Scott A. Smolka, and Bernhard Steffen. 1995. Reactive, generative, and stratified models of probabilistic processes. Information and Computation 121, 1 (1995), 59--80.
[40]
Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 5 (1994), 512--535.
[41]
Arnd Hartmanns and Holger Hermanns. 2015. In the quantitative automata zoo. Science of Computer Programming 112 (2015), 3--23.
[42]
Boudewijn Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, and Christel Baier. 2002. Model checking performability properties. In 3rd International Conference on Dependable Systems and Networks (DSN). 103--112.
[43]
Matthew Hennessy and Robin Milner. 1980. On observing nondeterminism and concurrency. In 7th International Colloquium on Automata, Languages and Programming (ICALP). Springer, 299--309. http://dl.acm.org/citation.cfm?id=646234.758793
[44]
Thomas A. Henzinger. 1996. The theory of hybrid automata. In 11th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 278--292.
[45]
Holger Hermanns. 2002. Interactive Markov chains: the quest for quantified quality. Springer.
[46]
Holger Hermanns, Jan Krcál, and Jan Kretínský. 2014. Probabilistic bisimulation: baturally on distributions. In 25th International Conference on Concurrency Theory (CONCUR) (Lecture Notes in Computer Science), Vol. 8704. Springer, 249--265.
[47]
Jianghai Hu, John Lygeros, and Shankar Sastry. 2000. Towards a theory of stochastic hybrid systems. In 12th International Conference on Hybrid Systems: Computation and Control (HSCC) (Lecture Notes in Computer Science), Vol. 1790. Springer, 160--173.
[48]
Claire Jones. 1990. Probabilistic non-determinism. Ph.D. Dissertation. University of Edinburgh.
[49]
Marcin Jurdzinski, Jeremy Sproston, and Francois Laroussinie. 2008. Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science 4, 3 (2008).
[50]
Olav Kallenberg. 2002. Foundations of modern probability. Springer.
[51]
Alexander S. Kechris. 1995. Classical descriptive set theory. Graduate Texts in Mathematics, Vol. 156. Springer.
[52]
Hans G. Kellerer. 1984. Duality theorems for marginal problems. Zeitschrift für Wahrscheinlichkeitstheorie und Verwandte Gebiete 67, 4 (1984), 399--432.
[53]
Vidyadhar G. Kulkarni. 1995. Modeling and analysis of stochastic systems. Chapman & Hall, Ltd.
[54]
Marta Kwiatkowska, Gethin Norman, Roberto Segala, and Jeremy Sproston. 2002. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science 282, 1 (2002), 101--150.
[55]
Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. 2007. Symbolic model checking for probabilistic timed automata. Information and Computation 205, 7 (2007), 1027--1077.
[56]
Kim G. Larsen and Arne Skou. 1991. Bisimulation through probabilistic testing. Information and Computation 94, 1 (1991), 1--28.
[57]
Lasse Leskelä. 2010. Stochastic relations of random variables and processes. Journal of Theoretical Probability 23, 2 (2010), 523--546.
[58]
Torgny Lindvall. 1992. Lectures on the coupling method. Wiley. http://opac.inria.fr/record=b1095731
[59]
Gabriel G. Infante López, Holger Hermanns, and Joost-Pieter Katoen. 2001. Beyond memoryless distributions: model checking semi-Markov chains. In 1st Joint International Workshop on Process Algebra and Probabilistic Methods - Performance Modelling and Verification (PAPM-PROBMIV). Springer, 57--70.
[60]
László Lovász. 2012. Large Networks and Graph Limits. American Mathematical Society. https://books.google.de/books?id=FsFqHLid8sAC
[61]
Martin R. Neuhäußer and Joost-Pieter Katoen. 2007. Bisimulation and logical preservation for continuous-time Markov decision processes. In 18th International Conference on Concurrency Theory (CONCUR). Springer, 412--427.
[62]
Gethin Norman, David Parker, and Jeremy Sproston. 2013. Model checking for probabilistic timed automata. Formal Methods in System Design 43, 2 (2013), 164--190.
[63]
Prakash Panangaden. 2009. Labelled Markov processes. Imperial College Press.
[64]
Roberto Segala. 1995. Modeling and verification of randomized distributed real-time systems. Ph.D. Dissertation. Massachusetts Institute of Technology.
[65]
Roberto Segala and Nancy Lynch. 1994. Probabilistic simulations for probabilistic processes. In 11th International Conference on Concurrency Theory (CONCUR). Springer, 481--496.
[66]
Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate. 2013. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems 12, 2 (2013), 921--956.
[67]
Shashi M. Srivastava. 2008. A course on Borel sets. Graduate texts in mathematics, Vol. 180. Springer.
[68]
Volker Strassen.1965. The existence of probability measures with given marginals. The Annals of Mathematical Statistics 36, 2 (1965), 423--439.
[69]
Pedro Sánchez Terraf. 2015. Bisimilarity is not Borel. Mathematical Structures in Computer Science (2015), 1--20.
[70]
Johan van Benthem. 1976. Modal correspondence theory. Ph.D. Dissertation. University of Amsterdam.
[71]
Cédric Villani. 2009. Optimal transport: old and new. Springer.
[72]
Nicolás Wolovick. 2012. Continuous probability and nondeterminism in labeled transitionsystems. Ph.D. Dissertation. FaMAF - Universidad Nacional de Córdoba.
[73]
Nicolás Wolovick and Sven Johr. 2006. A characterization of meaningful schedulers for continuous-time Markov decision processes. In 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS) (Lecture Notes in Computer Science), Vol. 4202. Springer, 352--367.
Index Terms
- Bisimulations, logics, and trace distributions for stochastic systems with rewards
Recommendations
Recursive stochastic games with positive rewards
AbstractWe study the complexity of a class of Markov decision processes and, more generally, stochastic games, called 1-exit Recursive Markov Decision Processes (1-RMDPs) and 1-exit Recursive Simple Stochastic Games (1-RSSGs), with strictly ...
Recursive Stochastic Games with Positive Rewards
ICALP '08: Proceedings of the 35th international colloquium on Automata, Languages and Programming - Volume Part IWe study the complexity of a class of Markov decision processes and, more generally, stochastic games, called 1-exit Recursive Markov Decision Processes (1-RMDPs) and Simple Stochastic Games (1-RSSGs) with strictly positive rewards. These are a class ...
Semi-Regenerative Processes with Unbounded Rewards
A semi-regenerative process SRP is combined with a reward structure such that the accumulated reward during [0, t] is the sum of a functional of the SRP and a functional of the embedded Markov renewal process MRP. For the expected discounted return a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
April 2018
296 pages
ISBN:9781450356428
DOI:10.1145/3178126
Copyright © 2018 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 11 April 2018
Check for updates
Qualifiers
- Research-article
- Research
- Refereed limited
Funding Sources
- DFG
- German Federal and State Governments
Conference
HSCC '18
Sponsor:
HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control
April 11 - 13, 2018
Porto, Portugal
Acceptance Rates
Overall Acceptance Rate 153 of 373 submissions, 41%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 222Total Downloads
- Downloads (Last 12 months)7
- Downloads (Last 6 weeks)1
Reflects downloads up to 22 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in