Combating Infinite State Using Ergo

  • Peter Robinson
  • Carron Shankland
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


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.


Model Check Modal Logic Label Transition System Sequent Calculus Full Formula 
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.


  1. 1.
    Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation 98, 142–170 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Hennessy, M., Lin, H.: Symbolic Bisimulations. Theoretical Computer Science 138, 353–389 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Calder, M., Maharaj, S., Shankland, C.: A Modal Logic for Full LOTOS based on Symbolic Transition Systems. The Computer Journal 45, 55–61 (2002)CrossRefzbMATHGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    International Organisation for Standardisation: Information Processing Systems — Open Systems Interconnection — LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour (1988) Google Scholar
  10. 10.
    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)CrossRefzbMATHGoogle Scholar
  11. 11.
    Pecheur, C.: Using LOTOS for specifying the CHORUS distributed operating system kernel. Computer Communications 15, 93–102 (1992)CrossRefGoogle Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the Association for Computing Machinery 32, 137–161 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Robinson, P., Staples, J.: Formalising a hierarchical structure of practical mathematical reasoning. Logic and Computation 3, 47–61 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Shankland, C., Calder, M.: Developing Implementation and Extending Theory: A Symbolic Approach to Reasoning about LOTOS. EPSRC project GR/M07779/01 (2002),
  17. 17.
    Broy, M., Merz, S., Spies, K.: Dagstuhl Seminar 1994. LNCS, vol. 1169. Springer, Heidelberg (1996)zbMATHGoogle Scholar
  18. 18.
    Ross, B.: Computing Symbolic Bisimulations. PhD thesis, University of Glasgow (2002) Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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),
  21. 21.
    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-07Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Peter Robinson
    • 1
  • Carron Shankland
    • 2
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandBrisbaneAustralia
  2. 2.Department of Computing Science and MathematicsUniversity of StirlingStirlingUK

Personalised recommendations