AbstractWe proposed a syntactic format, the panth format, for structured operational semantics in which besides ordinary transitions also predicates, negated predicates, and negative transitions may occur such that if the rules are stratifiable, strong bisimulation equivalence is a congruence for all the operators that can be defined within the panth format. To show that this format is useful we took some examples from the literature satisfying the panth format but no formats proposed by others. The examples touch upon issues such as priorities, termination, convergence, discrete time, recursion, (infinitary) Hennessy-Milner logic, and universal quantification.
Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory; F.1.1 [Computation by Abstract Devices]: Models of Computation; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages
Additional Key Words and Phrases: structured operational semantics, term deduction system, transition system specification, strong bisimulation, congruence theorem, predicate, negative premise, negated predicate, stratifiable, stratification
Selected papers that cite this one
- Roland Bol and Jan Friso Groote. The meaning of negative premises in transition system specifications. Journal of the ACM, 43(5):863-914, September 1996.
- Pedro R. D'Argenio and Chris Verhoef. A general conservative extension theorem in process algebras with inequalities. Theoretical Computer Science, 177(2):351-380, 15 May 1997.
- Wan Fokkink and Rob van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1-10, 10 April 1996.
- Wan Fokkink and Chris Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 10 October 1998.
Selected references
- Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229-239, San Diego, California, January 1988.
- Jan Friso Groote and Frits Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, October 1992.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.