On the consistency, expressiveness, and precision of partial modeling formalisms.

*(English)*Zbl 1214.68226Summary: Partial transition systems support abstract model checking of complex temporal properties by combining both over- and under-approximating abstractions into a single model. Over the years, three families of such modeling formalisms have emerged, represented by (1) Kripke modal transition systems (KMTSs), with restrictions on necessary and possible behaviors; (2) mixed transition systems (MixTSs), with relaxation on these restrictions; and (3) generalized Kripke MTSs (GKMTSs), with hyper-transitions, respectively.

In this paper, we investigate these formalisms based on two fundamental ways of using partial transition systems (PTSs) – as objects for abstracting concrete systems (and thus, a PTS is semantically consistent if it abstracts at least one concrete system) and as models for checking temporal properties (and thus, a PTS is logically consistent if it gives consistent interpretation to all temporal logic formulas). We study the connection between semantic and logical consistency of PTSs, compare the three families with respect to their expressive power (i.e., what can be modeled, what abstractions can be captured using them), and discuss the analysis power of these formalisms, i.e., the cost and precision of model checking.

Specifically, we identify a class of PTSs for which semantic and logical consistency coincide and define a necessary and sufficient structural condition to guarantee consistency. We also show that all three families of PTSs have the same expressive power (but do differ in succinctness). However, GKMTSs are more precise (i.e., can establish more properties) for model checking than the other two families. The direct use of GKMTSs in practice has been hampered by the difficulty of encoding them symbolically. We address this problem by developing a new semantics for temporal logic of PTSs that makes the MixTS family as precise for model checking as the GKMTS family. The outcome is a symbolic model checking algorithm that combines the efficient encoding of MixTSs with the model checking precision of GKMTSs. Our preliminary experiments indicate that the new algorithm is a good match for predicate-abstraction-based model checkers.

In this paper, we investigate these formalisms based on two fundamental ways of using partial transition systems (PTSs) – as objects for abstracting concrete systems (and thus, a PTS is semantically consistent if it abstracts at least one concrete system) and as models for checking temporal properties (and thus, a PTS is logically consistent if it gives consistent interpretation to all temporal logic formulas). We study the connection between semantic and logical consistency of PTSs, compare the three families with respect to their expressive power (i.e., what can be modeled, what abstractions can be captured using them), and discuss the analysis power of these formalisms, i.e., the cost and precision of model checking.

Specifically, we identify a class of PTSs for which semantic and logical consistency coincide and define a necessary and sufficient structural condition to guarantee consistency. We also show that all three families of PTSs have the same expressive power (but do differ in succinctness). However, GKMTSs are more precise (i.e., can establish more properties) for model checking than the other two families. The direct use of GKMTSs in practice has been hampered by the difficulty of encoding them symbolically. We address this problem by developing a new semantics for temporal logic of PTSs that makes the MixTS family as precise for model checking as the GKMTS family. The outcome is a symbolic model checking algorithm that combines the efficient encoding of MixTSs with the model checking precision of GKMTSs. Our preliminary experiments indicate that the new algorithm is a good match for predicate-abstraction-based model checkers.

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

##### Keywords:

partial transition systems; modal transition systems; 3-valued analysis; abstraction; model-checking
Full Text:
DOI

##### References:

[1] | A. Antonik, Decision Problems for Partial Specifications: Empirical and Worst-Case Complexity, Ph.D. Thesis, Imperial College, London, UK, September 2008. |

[2] | Antonik, A.; Huth, M., Efficient patterns for model checking partial state spaces in CTL intersection LTL, Electronic notes in theoretical computer science, 158, 41-57, (2006) · Zbl 1273.68218 |

[3] | A. Antonik, M. Huth, K.G. Larsen, U. Nyman, A. Wasowski, Complexity of decision problems for mixed and modal specifications, in: Proceedings of the 11th International Conference of Foundations of Software Science and Computational Structures (FOSSACS’08), LNCS, vol. 4962, March 2008, pp. 112-126. · Zbl 1139.68035 |

[4] | Antonik, A.; Huth, M.; Larsen, K.G.; Nyman, U.; Wasowski, A., EXPTIME-complete decision problems for modal and mixed specifications, Electronic notes in theoretical computer science, 242, 1, 19-33, (2009) · Zbl 1291.68172 |

[5] | Bagnara, R.; Hill, P.; Zaffanella, E., Widening operators for powerset domains, International journal on software tools for technology transfer (STTT), 8, 4-5, 449-466, (2006) |

[6] | G. Bruns, P. Godefroid, Model checking partial state spaces with 3-valued temporal logics, in: Proceedings of the 11th International Conference on Computer-Aided Verification (CAV’99), LNCS, vol. 1633, July 1999, pp. 274-287. · Zbl 1046.68583 |

[7] | G. Bruns, P. Godefroid, Generalized model checking: reasoning about partial state spaces, in: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00), LNCS, vol. 1877, August 2000, pp. 168-182. · Zbl 0999.68524 |

[8] | Chechik, M.; Devereux, B.; Easterbrook, S.; Gurfinkel, A., Multi-valued symbolic model-checking, ACM transactions on software engineering and methodology (TOSEM), 12, 4, 1-38, (2003) |

[9] | Cousot, P.; Cousot, R., Abstract interpretation frameworks, Journal of logic and computation, 2, 4, 511-547, (1992) · Zbl 0783.68073 |

[10] | Dams, D.; Gerth, R.; Grumberg, O., Abstract interpretation of reactive systems, ACM transactions on programming languages and systems (TOPLAS), 2, 19, 253-291, (1997) |

[11] | D. Dams, K.S. Namjoshi, The existence of finite abstractions for branching time model checking, in: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS’04), July 2004, pp. 335-344. |

[12] | D. Dams, K.S. Namjoshi, Automata as abstractions, in: Proceedings of the Sixth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’05), LNCS, vol. 3385, pp. 216-232. · Zbl 1112.68088 |

[13] | L. de Alfaro, P. Godefroid, R. Jagadeesan, Three-valued abstractions of games: uncertainty, but with precision, in: Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS’04), July 2004, pp. 170-179. |

[14] | P. Godefroid, M. Huth, Model checking vs. generalized model checking: semantic minimizations for temporal logics, in: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS’05), June 2005, pp. 158-167. |

[15] | P. Godefroid, R. Jagadeesan, On the expressiveness of 3-valued models, in: Proceedings of the Fourth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’03), LNCS, vol. 2575, January 2003, pp. 206-222. · Zbl 1022.68075 |

[16] | P. Godefroid, N. Piterman, LTL generalized model checking revisited, in: Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’09), LNCS, vol. 5403, January 2009, pp. 89-104. · Zbl 1206.68187 |

[17] | A. Gurfinkel, M. Chechik, How thorough is thorough enough, in: Proceedings of 13th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’05), LNCS, vol. 3725, October 2005, pp. 65-80. · Zbl 1159.68323 |

[18] | A. Gurfinkel, M. Chechik, Why waste a perfectly good abstraction? in: Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), LNCS, vol. 3920, March 2006, pp. 212-226. · Zbl 1180.68174 |

[19] | A. Gurfinkel, O. Wei, M. Chechik, Systematic construction of abstractions for model-checking, in: Proceedings of the Seventh International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), LNCS, vol. 3855, January 2006, pp. 381-397. · Zbl 1176.68121 |

[20] | A. Gurfinkel, O. Wei, M. Chechik, YASM: a software model-checker for verification and refutation, in: Proceedings of the 18th International Conference on Computer-Aided Verification (CAV’06), LNCS, vol. 4144, August 2006, pp. 170-174. |

[21] | Huth, M.; Jagadeesan, R.; Schmidt, D., A domain equation for refinement of partial systems, Mathematical structures in computer science, 14, 4, 469-505, (2004) · Zbl 1085.68090 |

[22] | M. Huth, R. Jagadeesan, D.A. Schmidt, Modal transition systems: a foundation for three-valued program analysis, in: Proceedings of 10th European Symposium on Programming (ESOP), LNCS, vol. 2028, April 2001, pp. 155-169. · Zbl 0987.68849 |

[23] | Kozen, D., Results on the propositional \(\mu\)-calculus, Theoretical computer science, 27, 334-354, (1983) · Zbl 0553.03007 |

[24] | K.G. Larsen, U. Nyman, A. Wasowski, On modal refinement and consistency, in: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR’07), LNCS, vol. 4703, September 2007, pp. 105-119. · Zbl 1151.68541 |

[25] | K.G. Larsen, B. Thomsen, A modal process logic, in: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), July 1988, pp. 203-210. |

[26] | P. Larsen, The expressive power of implicit specifications, in: Proceedings of the 18th International Colloquium on Automata, Languages and Programming (ICALP’91), LNCS, vol. 510, July 1991, pp. 204-216. · Zbl 0785.68062 |

[27] | S. Nejati, M. Gheorghiu, M. Chechik, Thorough checking revisited, in: Proceedings of the Sixth International Conference on Formal Methods in Computer-Aided Design (FMCAD’06), November 2006, pp. 106-116. |

[28] | T.W. Reps, A. Loginov, S. Sagiv, Semantic minimization of 3-valued propositional formulae, in: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS’02), July 2002, pp. 40-54. |

[29] | S. Shoham, O. Grumberg, Monotonic abstraction-refinement for CTL, in: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’04), LNCS, vol. 2988, March 2004, pp. 546-560. · Zbl 1126.68487 |

[30] | S. Shoham, O. Grumberg, 3-Valued abstraction: more precision at less cost, in: Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS’06), August 2006, pp. 399-410. |

[31] | F. Somenzi, CUDD: CU Decision Diagram Package Release, 2001. |

[32] | O. Wei, A. Gurfinkel, M. Chechik, Mixed transition systems revisited, in: Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’09), LNCS, vol. 5403, January 2009, pp. 349-365. · Zbl 1206.68194 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.