Abstract
Witnesses and counterexamples produced by model checkers provide a very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specified with a CCS-like process algebra. There, only linear and finite witnesses and counterexamples are useful and for the given formula and model an efficient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identifies a fragment of action computation tree logic (ACTL) that can be handled in this way. Moreover, a suitable form of witnesses and counterexamples is proposed and witness and counterexample automata are introduced, which are finite automata recognizing them. An algorithm for generating such automata is given.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-3-540-30232-2_24
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. Journal of computer and syst. sciences 62(3), 463–515 (2001)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM Transaction on Programming Languages and Systems 5(16), 1512–1542 (1994)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite State Concurrent Systems using Temporal Logic Specifications. ACM Transaction on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like Counterexamples in Model Checking. In: 17th IEEE Symp. on Logic in Computer Science (LICS), pp. 19–29 (2002)
Copty, F., Irron, A., Weissberg, O., Kropp, N., Kamhi, G.: Efficient Debugging in a Formal Verification Environment. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 275–292. Springer, Heidelberg (2001)
Časar, A., Brezočnik, Z., Kapus, T.: Exploiting Symbolic Model Checking for Sensing Stuck-at Faults in Digital Circuits. Informacije MIDEM 32(3), 171–180 (2002)
Fantechi, A., Gnesi, S., Maggiore, A.: Enhancing test coverage by back-tracing model-checker counterexamples. In: Int. Workshop on Test and Analysis of Component Based Syst, TACOS (2004); to appear in Electronic Notes in Theoretical Computer Science
Geist, D., Farkas, M., Landver, A., Lichenstein, Y., Ur, S., Wolfsthal, Y.: Coverage- Directed Test Generation Using Symbolic Techniques. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 143–158. Springer, Heidelberg (1996)
Glusman, M., Kamhi, G., Mador-Heim, S., Fraer, R., Vardi, M.: Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 176–191. Springer, Heidelberg (2003)
Gurfinkel, A., Chechik, M.: Proof-Like Counter-Examples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 160–175. Springer, Heidelberg (2003)
Ho, P.H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart Simulation Using Collaborative Formal and Simulation Engines. In: Int. Conf. on Computer Aided Design, ICCAD (2000)
Maidl, M.: The Common Fragment of CTL and LTL. In: Proc. 41th Symp. on Foundations of Computer Science (FOCS), pp. 643–652 (2000)
De Nicola, R., Vaandrager, F.W.: Actions versus State Based Logics for Transition Systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Ratzaby, G., Ur, S., Wolfsthal, Y.: Coverability Analysis Using Symbolic Model Checking. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, p. 155. Springer, Heidelberg (2001)
Ratsaby, G., Sterin, B., Ur, S.: Improvements in Coverabiliy Analysis. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, p. 41. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 IFIP International Federation for Information Processing
About this paper
Cite this paper
Meolic, R., Fantechi, A., Gnesi, S. (2004). Witness and Counterexample Automata for ACTL. In: de Frutos-Escrig, D., Núñez, M. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2004. FORTE 2004. Lecture Notes in Computer Science, vol 3235. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30232-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-30232-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23252-0
Online ISBN: 978-3-540-30232-2
eBook Packages: Springer Book Archive