Cited By
View all- Perez INilsson H(2017)Testing and debugging functional reactive programmingProceedings of the ACM on Programming Languages10.1145/31102461:ICFP(1-27)Online publication date: 29-Aug-2017
Stuttering Abstraction for Model Checkin
Pages 311 - 320
Abstract
Abstraction is one of the most effective approaches to improving the applicability and the scalability of modelchecking. The goal of abstraction is to construct a model which is small enough to analyze, yet contains enough detail to allow conclusive analysis of properties of interest. For a given concrete model, the size of its smallest possible abstraction is intimately related to the set of temporal properties preserved by the abstraction. Thus, smaller abstractions are possible if we reduce this set, for example, by disallowing the use of the next-time operator. In this paper, we improve the conclusiveness and efficiency of the 3-valued abstraction framework. We start by proposing a number of simulation relations that preserve true properties expressed in subsets of CTL without the next-time operator. We show how these simulation relations are extended into refinement relations for defining 3-valued abstractions. Using these refinement relations, we give a new abstraction method that results in more conclusive abstract models.
References
[1]
M. Abadi and L. Lamport. "The Existence of Refinement Mappings". Theor. Computer Science, 82(2):253-284, 1991.
[2]
T. Ball, A. Podelski, and S. Rajamani. "Boolean and Cartesian Abstraction for Model Checking C Programs". In TACAS, vol. 2031 of LNCS, 2001.
[3]
M. C. Browne, E. M. Clarke, and O. Grumberg. "Characterizing Finite Kripke Structures in Propositional Temporal Logic". Theor. Computer Science, 59(1-2):115-131, 1988.
[4]
S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. "Modular Verification of Software Components in C". In ICSE, pp. 385-395, 2003.
[5]
E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. "Counterexample-Guided Abstraction Refinement". In CAV, vol. 1855 of LNCS, pp. 154-169, 2000.
[6]
E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
[7]
D. Dams. Abstract Interpretation and Partition Refinement for Model Checking. PhD thesis, Eindhoven University of Technology, July 1996.
[8]
D. Dams, R. Gerth, and O. Grumberg. "Abstract Interpretation of Reactive Systems". ACM Transactions on Programming Languages and Systems, 2(19):253- 291, 1997.
[9]
D. Dams and K. Namjoshi. "The Existence of Finite Abstractions for Branching Time Model Checking". In LICS, 2004.
[10]
D. Dams and K. Namjoshi. "Automata as Abstractions". In VMCAI, 2005.
[11]
L. de Alfaro, P. Godefroid, and R. Jagadeesan. "Three-Valued Abstractions of Games: Uncertainty, but with Precision". In LICS, 2004.
[12]
P. Godefroid, M. Huth, and R. Jagadeesan. "Abstraction-based Model Checking using Modal Transition Systems". In CONCUR, vol. 2154 of LNCS, 2001.
[13]
P. Godefroid and R. Jagadeesan. "On the Expressiveness of 3-Valued Models". In VMCAI, vol. 2575 of LNCS, pp. 206-222, 2003.
[14]
S. Graf and H. Saïdi. "Construction of Abstract State Graphs with PVS". In CAV, vol. 1254 of LNCS, 1997.
[15]
T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. "Lazy abstraction". In POPL, pp. 58-70, 2002.
[16]
M. Huth, R. Jagadeesan, and D. A. Schmidt. "Modal Transition Systems: A Foundation for Three-Valued Program Analysis". In ESOP, vol. 2028 of LNCS, 2001.
[17]
S. C. Kleene. Introduction to Metamathematics. New York: Van Nostrand, 1952.
[18]
L. Lamport. "What Good is Temporal Logic?". In IFlP 9th World Computer Congress, vol. 83 of Information Processing, pp. 657-668, 1983.
[19]
K.G. Larsen and B. Thomsen. "A Modal Process Logic". In LICS, 1988.
[20]
K.G. Larsen and L. Xinxin. "Equation solving using modal transition systems". In LICS, 1990.
[21]
L. Libkin. Elements of Finite Model Theory. Springer-Verlag, 2003.
[22]
P. Manolios. "Mechanical Verification of Reactive Systems". PhD thesis, University of Texas. Austin, 2001.
[23]
R. Milner. "An Algebraic Definition of Simulation between Programs". In 2nd Inter. Joint Conf. on AI, pp. 481-489, 1971.
[24]
S. Nejati. "Refinement Relations on Partial Specifications". Master's thesis, Univ. of Toronto, July 2003.
[25]
S. Nejati. "Formal Analysis of the Alternating Bit Protocol Using Stuttering Refinement". CSRG Tech. Report 487, Univ. of Toronto, 2004.
[26]
S. Nejati, A. Gurfinkel, and M. Chechik. "Stuttering Abstraction for Model Checking". CSRG Tech. Report 526, Univ. of Toronto, 2005.
[27]
R. De Nicola and F. Vaandrager. "Three Logics for Branching Bisimulation". J. of the ACM. 42(2):458- 487, 1995.
[28]
S. Shoham and O. Grumberg. "Monotonic Abstraction-Refinement for CTL". In TACAS, vol. 2988 of LNCS, 2004.
Index Terms
- Stuttering Abstraction for Model Checkin
Recommendations
Abstraction for model checking multi-agent systems
Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel ...
3-Valued Abstraction for (Bounded) Model Checking
ATVA '09: Proceedings of the 7th International Symposium on Automated Technology for Verification and AnalysisModel Checking is the problem of verifying that a given model satisfies a specification, given in a formal specification language. Abstraction is one of the most successful approaches to avoiding the state explosion problem in model checking. It ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2005
433 pages
ISBN:0769524354
Publisher
IEEE Computer Society
United States
Publication History
Published: 07 September 2005
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 17 Dec 2024
Other Metrics
Citations
Cited By
View all- Perez INilsson H(2017)Testing and debugging functional reactive programmingProceedings of the ACM on Programming Languages10.1145/31102461:ICFP(1-27)Online publication date: 29-Aug-2017