Eventuality in LOTOS with a Disjunction Operator

  • Yoshinao Isobe
  • Yutaka Sato
  • Kazuhito Ohmaki
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1538)


LOTOS is a formal specification language, designed for the precise description of open distributed systems and protocols. Our purpose is to introduce the operators of logics (for example, disjunction, conjunction, greatest fixpoint, least fixpoint in μ-calculus) into (basic) LOTOS, in order to describe flexible specifications. Disjunction operators ∨ have been already proposed for expressing two or more implementations in a flexible pecification. In this paper, we propose an extended LOTOS with two state operators. They can control recursive behavior, in order to express eventuality. The eventuality is useful for liveness properties that something good must eventually happen. Then, we present a method for checking the consistency of a number of flexible specifications, and a method for producing a conjunction specification of them


Stable State Standard Form Unstable State Internal Action Label Transition System 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Barbuti: Selective mu-calculus: New Modal Operators for Proving Properties on Reduced Transition Systems, Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X/PSTV XVII, pp. 519–534, 1997.Google Scholar
  2. 2.
    E. Brinksma: Constraint-oriented specification in a constructive formal description technique, LNCS 430, Springer-Verlag, pp. 130–152, 1989.Google Scholar
  3. 3.
    P.J.B. Glabbeek and W.P. Weijland: Branching Time and Abstraction in Bisimulation Semantics, Journal of the ACM, Vol. 43, No. 3, pp. 555–600, 1996.CrossRefMathSciNetGoogle Scholar
  4. 4.
    C.A.R. Hoare: Communicating Sequential Processes, Prentice-Hall, 1985.Google Scholar
  5. 5.
    Y. Isobe, H. Nakada, Y. Sato, and K. Ohmaki: Stepwise Synthesis of Multi-Specifications using Static Choice Actions (in Japanese). Foundation of Software Engineering IV (FOSE’97), Lecture Notes 19, Kindaikagaku-sha, pp. 12–19, 1997.Google Scholar
  6. 6.
    P.C. Kanellakis and S.A. Smolka: CCS Expressions, Finite State Processes, and Three Problems of Equivalence, Information and Computation, Vol. 86, pp. 43–68, 1990.zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    S. Kimura, A. Togashi and N. Shiratori: Synthesis Algorithm for Recursive Processes by μ-calculus, Algorithmic Learning Theory, LNCS 872, Springer-Verlag, pp. 379–394, 1994.Google Scholar
  8. 8.
    K.G. Larsen: Modal Specifications, Automatic Verification Methods for Finite State Systems, LNCS 407, Springer-Verlag, pp. 232–246, 1989.Google Scholar
  9. 9.
    K.G. Larsen: The expressive Power of Implicit Specifications, Automata, Languages and Programming, LNCS 510, Springer-Verlag, pp. 204–216, 1991.Google Scholar
  10. 10.
    K.G. Larsen, B. Steffen, and C. Weise: A Constraint Oriented Proof Methodology Based on Modal Transition Systems, Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1019, Springer-Verlag, pp. 17–40, 1995.Google Scholar
  11. 11.
    Z. Manna and P. Wolper: Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Trans. on Programming Languages and Systems, Vol. 6, No. 1, pp. 67–93, 1984.CrossRefGoogle Scholar
  12. 12.
    R. Milner: Communication and Concurrency, Prentice-Hall, 1989.Google Scholar
  13. 13.
    M.W.A. Steen, H. Bowman, and J. Derrick: Composition of LOTOS specification, Protocol Specification, Testing and Verification, XV, pp. 73–88, 1995Google Scholar
  14. 14.
    M.W.A. Steen, H. Bowman, J. Derrick, and E.A. Boiten,: Disjunction of LOTOS specification, Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X/PSTV XVII, pp. 177–192, 1997.Google Scholar
  15. 15.
    Colin Stirling: An Introduction to Modal and Temporal Logics for CCS, Concurrency: Theory, Language, and Architecture, LNCS 491, Springer-Verlag, pp. 2–20, 1989.Google Scholar
  16. 16.
    D.J. Walker: Bisimulations and Divergence, Proc. of third annual IEEE symposium on Logic in Computer Science, pp. 186–192, 1988.Google Scholar
  17. 17.
    ISO 8807: Information Processing Systems-Open System Interconnection—LOTOS—A formal description technique based on the temporal ordering of observational behavior, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Yoshinao Isobe
    • 1
  • Yutaka Sato
    • 1
  • Kazuhito Ohmaki
    • 1
  1. 1.Electrotechnical LaboratoryIbarakiJapan

Personalised recommendations