Abstract.
Symbolic transition systems can be used to represent infinite state systems in a finite manner. The modal logic FULL, defined over symbolic transition systems, allows properties over infinite state to be expressed, establishing necessary constraints on data. We present here a theory and tactics for FULL, developed using Ergo, a generalised sequent calculus style theorem prover allowing interactive proofs. This allows exploitation of the underlying symbolic transition system and reasoning about symbolic values.
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
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98, 142–170 (1992)
Clarke, E., Filkorn, T., Jha, S.: Exploiting Symmetry In Temporal Logic Model Checking. In: Courcoubetis, C. (ed.) Proceedings of the 5thWorkshop on Computer-Aided Verification, pp. 450–462. Springer, Heidelberg (1993)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W. (ed.) Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, Heidelberg (1999)
Bharadwaj, R., Sims, S.: Salsa: Combining constraint solvers with BDDs for automated invariant checking. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000 (2000)
Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138, 353–389 (1995)
Calder, M., Shankland, C.: A Symbolic Semantics and Bisimulation for Full LOTOS. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems, pp. 184–200. Kluwer Academic Publishers, Dordrecht (2001)
Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS based on Symbolic Transition Systems. The Computer Journal 45, 55–61 (2002)
Utting, M., Robinson, P., Nickson, R.: A Generic Proof Engine that uses Prolog Proof Technology. London Mathematical Society Journal of Computation and Mathematics 5 (2002)
International Organisation for Standardisation: Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour (1988)
Sighireanu, M., Mateescu, R.: Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): an Experiment with E-LOTOS. Springer International Journal on Software Tools for Technology Transfer (STTT) 2, 68–88 (1998)
Pecheur, C.: Using LOTOS for specifying the CHORUS distributed operating system kernel. Computer Communications 15, 93–102 (1992)
Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437–440. Springer, Heidelberg (1996)
Calder, M., Maharaj, S., Shankland, C.: An Adequate Logic for Full LOTOS. In: Oliveira, J., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 384–395. Springer, Heidelberg (2001)
Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery 32, 137–161 (1985)
Robinson, P., Staples, J.: Formalising a hierarchical structure of practical mathematical reasoning. Logic and Computation 3, 47–61 (1993)
Shankland, C., Calder, M.: Developing Implementation and Extending Theory: A Symbolic Approach to Reasoning about LOTOS. EPSRC project GR/M07779/01 (2002), http://www.cs.stir.ac.uk/diet/
Broy, M., Merz, S., Spies, K.: Dagstuhl Seminar 1994. LNCS, vol. 1169. Springer, Heidelberg (1996)
Ross, B.: Computing Symbolic Bisimulations. PhD thesis, University of Glasgow (2002)
Bryans, J., Shankland, C.: Implementing a modal logic over data and processes using XTL. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of FORTE 2001, 21st International Conference on Formal Techniques for Networked and Distributed Systems, pp. 201–218. Kluwer Academic Publishers, Dordrecht (2001)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and Programming in Rewriting Logic. SRI International (January 1999) (revised, August 1999), http://maude.csl.sri.com
Bryans, J., Verdejo, A., Shankland, C.: Using Rewriting Logic to implement the modal logic FULL. In: Bharadwaj, R. (ed.): AVIS 2001: First International Workshop on Automated Verification of Infinite-State Systems, Naval Research Laboratory Technical Memorandum (2001): Also in Nowak, D. (ed.) AVoCS 2001: Workshop on Automated Verification of Critical Systems, Oxford University Computing Laboratory technical report PRG-RR-01-07
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Robinson, P., Shankland, C. (2003). Combating Infinite State Using Ergo. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive