More Web Proxy on the site http://driver.im/

research-article

Incremental Bisimulation Abstraction Refinement

Authors:

Holger Hermanns,

Jens CHR. GodskesenAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 13, Issue 4s

Article No.: 142, Pages 1 - 23

https://doi.org/10.1145/2627352

Published: 28 July 2014 Publication History

Abstract

Abstraction refinement techniques in probabilistic model checking are prominent approaches for verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This article proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.

References

[1]

Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, David L. Dill, and Howard Wong-Toi. 1992. Minimization of timed transition systems. In Proceedings of the 3rd International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 630. Springer-Verlag, 340--354. http://dl.acm.org/citation.cfm&quest;id=646727.703209

Digital Library

[2]

James Aspnes and Maurice herlihy. 1990. Fast randomized consensus using shared memory. J. Algor. 11, 3 (1990), 441--461. http://dx.doi.org/10.1016/0196-6774(90)90021-6

Digital Library

[3]

Christel Baier, Bettina Engelen, and Mila Majster-Cederbaum. 2000. Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60, 1 (2000), 187--231. http://dx.doi.org/10.1006/jcss.1999.1683

Digital Library

[4]

Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.

Digital Library

[5]

Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. 2005. Comparative branching-time semantics for Markov chains. Inf. Comput. 200, 2 (2005), 149--214.

Digital Library

[6]

Joffroy Beauquier, Maria Gradinariu, and Colette Johnen. 1999. Memory space requirements for self-stabilizing leader election protocols. In Proceedings of the 18th Annual ACM Symposium on Principles of Distributed Computing (PODC'99). ACM, 199--207. http://doi.acm.org/10.1145/301308.301358

Digital Library

[7]

Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, and Pascal Raymond. 1992. Minimal state graph generation. Sci. Comput. Program. 18, 3 (1992), 247--269. http://dx.doi.org/10.1016/0167-6423(92) 90018-7

Digital Library

[8]

Rohit Chadha and Mahesh Viswanathan. 2010. A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Trans. Comput. Logic 12, 1 (2010), 1:1--1:49. http://doi.acm.org/10.1145/1838552.1838553

Digital Library

[9]

Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5 (2003), 752--794. http://doi.acm.org/10.1145/876638.876643

Digital Library

[10]

Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2 (1986), 244--263.

Digital Library

[11]

Pedro R. D'Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen, and Kim Guldstrand Larsen. 2001. Reachability analysis of probabilistic systems by successive refinements. In Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification. Lecture Notes in Computer Science, vol. 2165, Springer-Verlag, 39--56. http://dl.acm.org/citation.cfm&quest;id=645776.668429

Digital Library

[12]

Pedro R. D'Argenio, Bertrand Jeannet, Henrik Ejersbo Jensen, and Kim Guldstrand Larsen. 2002. Reduction and refinement strategies for probabilistic analysis. In Proceedings of the 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification. Lecture Notes in Computer Science, vol. 2399, Springer-Verlag, 57--76. http://dl.acm.org/citation.cfm&quest;id=645777.668444

Digital Library

[13]

Luca de Alfaro and Pritam Roy. 2007. Magnifying-lens abstraction for Markov decision processes. In Proceedings of the 19th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, Springer-Verlag, 325--338. http://dl.acm.org/citation.cfm&quest;id=1770351.1770402

Digital Library

[14]

Christian Dehnert. 2011. Symbolic Bisimulation Minimization of Markov Models. Master's thesis. RWTH Aachen University. Diplomarbeit.

[15]

Christian Dehnert, Joost-Pieter Katoen, and David Parker. 2013. SMT-based bisimulation minimisation of Markov models. In Proceedings of the 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 7737, Springer, 28--47. http://dblp.uni-trier.de/db/conf/vmcai/vmcai2013.html&num;DehnertKP13

[16]

Salem Derisavi, Holger Hermanns, and William H. Sanders. 2003. Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87, 6 (2003), 309--315. http://dx.doi.org/10.1016/S0020-0190(03)00343-0

Digital Library

[17]

Josée Desharnais, Mathieu Tracol, and Abir Zhioua. 2011. Computing distances between probabilistic automata. In Proceedings of the 9th Workshop on Quantitative Aspects of Programming Languages (QAPL'11). 148--162.

[18]

Javier Esparza and Andreas Gaiser. 2011. Probabilistic abstractions with arbitrary domains. In Proceedings of the 18th International Conference on Static Analysis. Lecture Notes in Computer Science, vol. 6887, Springer-Verlag, 334--350. http://dl.acm.org/citation.cfm&quest;id=2041552.2041577

Digital Library

[19]

Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang. 2010. PASS: Abstraction refinement for infinite probabilistic models. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, Javier Esparza and Rupak Majumdar (Eds.), vol. 6015, Springer, 353--357.

Digital Library

[20]

Paul Richard Halmos. 1974. Measure Theory. Graduate Texts in Mathematics, Book 18. Springer-Verlag, New York, NY.

[21]

Hans Hansson and Bengt Jonsson. 1994. A logic for reasoning about time and reliability. Formal Asp. Comput. 6, 5 (1994), 512--535. http://dx.doi.org/10.1007/BF01211866

Digital Library

[22]

Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. 2011. Probabilistic logical characterization. Inf. Comput. 209, 2 (2011), 154--172. http://dx.doi.org/10.1016/j.ic.2010.11.024

Digital Library

[23]

Holger Hermanns, Björn Wachter, and Lijun Zhang. 2008. Probabilistic CEGAR. In Proceedings of the 20th International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 5123, Springer-Verlag, 162--175. http://dx.doi.org/10.1007/978-3-540-70545-1_16

Digital Library

[24]

Amos Israeli and Marc Jalfon. 1990. Token management schemes and random walks yield self-stabilizing mutual exclusion. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing (PODC'90). ACM, 119--131. http://doi.acm.org/10.1145/93385.93409

Digital Library

[25]

Alon Itai and Michael Rodeh. 1990. Symmetry breaking in distributed networks. Inf. Comput. 88, 1 (July 1990), 60--87. http://dx.doi.org/10.1016/0890-5401(90)90004-2

Digital Library

[26]

Bengt Jonsson and Kim Guldstrand Larsen. 1991. Specification and refinement of probabilistic processes. In Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS'91). IEEE Computer Society, 266--277. http://dx.doi.org/10.1109/LICS.1991.151651

[27]

Joost-Pieter Katoen, Tim Kemna, Ivan Zapreev, and David N. Jansen. 2007. Bisimulation minimisation mostly speeds up probabilistic model checking. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4424, Springer-Verlag, 87--101. http://dl.acm.org/citation.cfm&quest;id=1763507.1763519

Digital Library

[28]

Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, and David Parker. 2009. Abstraction refinement for probabilistic software. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 5403, Springer-Verlag, 182--197. http://dx.doi.org/10.1007/978-3-540-93900-9_17

Digital Library

[29]

Mark Kattenbelt, Marta Kwiatkowska, Gethin Norman, and David Parker. 2010. A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36, 3 (2010), 246--280. http://dx.doi.org/10.1007/s10703-010-0097-6

Digital Library

[30]

Marta Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of probabilistic real-time systems. In Proceedings of the 23rd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6806, Springer-Verlag, 585--591. http://dl.acm.org/citation.cfm&quest;id=2032305.2032352

Digital Library

[31]

Kim G. Larsen. 1990. In Automatic Verification Methods for Finite State Systems. Lecture Notes in Computer Science, vol. 407, Springer-Verlag, 232--246.

[32]

Pritam Roy, David Parker, Gethin Norman, and Luca de Alfaro. 2008. Symbolic magnifying lens abstraction in markov decision processes. In Proceedings of the 5th International Conference on Quantitative Evaluation of Systems (QEST'08). IEEE Computer Society, 103--112.

Digital Library

[33]

Walter Rudin. 2006. Real and Complex Analysis. Tata McGraw-Hill Education.

[34]

Roberto Segala. 1995. Modeling and verification of randomized distributed realtime systems. Ph.D. Dissertation. MIT.

Digital Library

[35]

Roberto Segala and Nancy Lynch. 1995. Probabilistic simulations for probabilistic processes. Nordic J. of Computing 2, 2 (1995), 250--273. http://dl.acm.org/citation.cfm&quest;id=642068.642075

Digital Library

[36]

Lei Song, Lijun Zhang, Jens Chr. Godskesen, and Flemming Nielson. 2013a. Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods Comput. Sci. 9, 2:7 (2013).

[37]

Lei Song, Lijun Zhang, Holger Hermanns, and Jens Chr Godskesen. 2013b. Incremental bisimulation abstraction refinement. In Proceedings of the 13th International Conference on Application of Concurrency to System Design (ACSD'13). IEEE Computer Society, 11--20.

Digital Library

[38]

R. F. Lutje Spelberg, Hans Toetenel, and Marcel Ammerlaan. 1998. Partition refinement in real-time model checking. In Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 1486, Springer-Verlag, 143--157. http://dl.acm.org/citation.cfm&quest;id=646845.706939

Digital Library

[39]

Antti Valmari and Giuliana Franceschinis. 2010. Simple O(m log n) time Markov chain lumping. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 6015, Springer-Verlag, 38--52.

Digital Library

[40]

Björn Wachter and Lijun Zhang. 2010. Best probabilistic transformers. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 5944, Springer-Verlag, 362--379. http://dx.doi.org/10.1007/978-3-642-11319-2_26

Digital Library

[41]

Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, and Bernd Becker. 2006. Sigref: A symbolic bisimulation tool box. In Proceedings of the 4th International Conference on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 4218, Springer-Verlag, 477--492. http://dx.doi.org/10.1007/11901914_35

Digital Library

[42]

Lijun Zhang and Holger Hermanns. 2007. Deciding simulations on probabilistic automata. In Proceedings of the 5th International Conference on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 4762, Springer-Verlag, 207--222. http://dl.acm.org/citation.cfm&quest;id=1779046.1779064

Digital Library

Cited By

Szekeres DMarussy KMajzik I(2024)A Lazy Abstraction Algorithm for Markov Decision ProcessesAnalytical and Stochastic Modelling Techniques and Applications10.1007/978-3-031-70753-7_6(81-96)Online publication date: 14-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-70753-7_6
Szekeres DMajzik I(2023)Towards Abstraction-based Probabilistic Program AnalysisActa Cybernetica10.14232/actacyb.29828726:3(671-711)Online publication date: 2-Jun-2023
https://doi.org/10.14232/actacyb.298287
Garavel HLang F(2022)Equivalence Checking 40 Years After: A Review of Bisimulation ToolsA Journey from Process Algebra via Timed Automata to Model Learning10.1007/978-3-031-15629-8_13(213-265)Online publication date: 7-Sep-2022
https://doi.org/10.1007/978-3-031-15629-8_13
Show More Cited By

Incremental Bisimulation Abstraction Refinement

Recommendations

Incremental Bisimulation Abstraction Refinement
ACSD '13: Proceedings of the 2013 13th International Conference on Application of Concurrency to System Design

Abstraction refinement techniques in probabilistic model checking are prominent approaches to the verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of ...
An abstraction refinement approach combining precise and approximated techniques

Predicate abstraction is a powerful technique to reduce the state space of a program to a finite and affordable number of states. It produces a conservative over-approximation where concrete states are grouped together according to a given set of ...
Counterexample guided abstraction refinement of product-line behavioural models
FSE 2014: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering

The model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 13, Issue 4s

Special Issue on Real-Time and Embedded Technology and Applications, Domain-Specific Multicore Computing, Cross-Layer Dependable Embedded Systems, and Application of Concurrency to System Design (ACSD'13)

July 2014

571 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/2601432

Editors:
Sandeep K. Shukla
Virginia Tech, USA
,
Josep Carmona
Universitat Politècnica de Catalunya, Spain
,
Mihai Teodor Lazarescu
Politecnico di Torino, Italy
,
Marta Pietkiewicz-koutny
Newcastle University, UK

Issue’s Table of Contents

Copyright © 2014 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 ACM 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 28 July 2014

Accepted: 01 February 2014

Received: 01 October 2013

Published in TECS Volume 13, Issue 4s

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
132
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Szekeres DMarussy KMajzik I(2024)A Lazy Abstraction Algorithm for Markov Decision ProcessesAnalytical and Stochastic Modelling Techniques and Applications10.1007/978-3-031-70753-7_6(81-96)Online publication date: 14-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-70753-7_6
Szekeres DMajzik I(2023)Towards Abstraction-based Probabilistic Program AnalysisActa Cybernetica10.14232/actacyb.29828726:3(671-711)Online publication date: 2-Jun-2023
https://doi.org/10.14232/actacyb.298287
Garavel HLang F(2022)Equivalence Checking 40 Years After: A Review of Bisimulation ToolsA Journey from Process Algebra via Timed Automata to Model Learning10.1007/978-3-031-15629-8_13(213-265)Online publication date: 7-Sep-2022
https://doi.org/10.1007/978-3-031-15629-8_13
Groote JRivera Verduzco JDe Vink E(2018)An Efficient Algorithm to Determine Probabilistic BisimulationAlgorithms10.3390/a1109013111:9(131)Online publication date: 3-Sep-2018
https://doi.org/10.3390/a11090131
Lee SYoon SKim JKim S(2018)Adaptive correlated prefetch with large-scale hybrid memory system for stream processingThe Journal of Supercomputing10.1007/s11227-018-2466-774:9(4746-4770)Online publication date: 1-Sep-2018
https://dl.acm.org/doi/10.1007/s11227-018-2466-7
Sanchez Mde la Oliva ABernardos C(2016)Experimental analysis of connectivity management in mobile operating systemsComputer Networks: The International Journal of Computer and Telecommunications Networking10.1016/j.comnet.2015.11.02194:C(41-61)Online publication date: 15-Jan-2016
https://dl.acm.org/doi/10.1016/j.comnet.2015.11.021

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents