Abstract
We present a general theory for the use of negative premises in the rules of Transition System Specifications (TSS's). We formulate a criterion that should be satisfied by a TSS in order to be meaningful, i.e. to unequivocally define a transition relation. We also provide powerful techniques for proving that a TSS satisfies this criterion, meanwhile constructing this transition relation. Both the criterion and the techniques originate from logic programming [8, 7] to which TSS's are close.
As in [10], we show that the bisimulation relation induced by a TSS is a congruence, provided that it is in ntyft/ntyxt-format and can be proved meaningful using our techniques. As a running example, we study the combined addition of priorities and abstraction to Basic Process Algebra (BPA). Under some reasonable conditions we show that this TSS is indeed meaningful, which could not be shown by other methods [2, 10]. Finally, we provide a sound and complete axiomatization for this example. We have omitted most proofs here; they can be found in [3].
The first author is partly supported by the European Communities under ESPRIT Basic Research Action 3020 (Integration). The second author is supported by the European Communities under RACE project no. 1046 (SPECS) and ESPRIT Basic Research Action 3006 (CONCUR).
(Extended Abstract)
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fund. Inf., XI(2):127–168, 1986.
B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced: preliminary report. In Conference Record of the 15th ACM Symposium on Principles of Programming Languages, San Diego, California, pages 229–239, 1988.
R.N. Bol and J.F. Groote. The meaning of negative premises in transition system specifications. Report CS-R9054, CWI, Amsterdam, 1990.
T. Bolognesi, F. Lucidi, and S. Trigila. From timed Petri nets to timed LOTOS. In L. Logrippo, R.L. Probert, and H. Ural, editors, Proceedings of the Tenth International IFIP WG6.1 Symposium on Protocol Specification, Testing and Verification, Ottawa, 1990.
J. Camilleri. An operational semantics for OCCAM. International Journal of Parallel Programming, 18(5):149–167, October 1989.
R. Cleaveland and M. Hennessy. Priorities in process algebra. In Proceedings third Annual Symposium on Logic in Computer Science (LICS), Edinburgh, pages 193–202, 1988.
A. van Gelder, K. Ross, and J.S. Schlipf. Unfounded sets and well-founded semantics for general logic programs. In Proceedings of the Seventh Symposium on Principles of Database Systems, pages 221–230. ACM SIGACT-SIGMOD, 1988.
M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In R. Kowalski and K. Bowen, editors, Proceedings of the Fifth Logic Programming Symposium, pages 1070–1080. MIT press, 1988.
R.J. van Glabbeek. Bounded nondeterminism and the approximation induction principle in process algebra. In F.J. Brandenburg, G. Vidal-Naquet, and M. Wirsing, editors, Proceedings STACS 87, LNCS 247, pages 336–347. Springer-Verlag, 1987.
J.F. Groote. Transition system specifications with negative premises. Technical Report CS-R8950, CWI, Amsterdam, 1989. An extended abstract appeared in J.C.M. Baeten and J.W. Klop, editors, Proceedings of Concur90, Amsterdam, LNCS 458, pages 332–341. Springer-Verlag, 1990.
J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Technical Report CS-R8845, CWI, Amsterdam, 1988. An extended abstract appeared in G. Ausiello, M. Dezani-Ciancaglini and, S. Ronchi Della Rocca, editors, Proceedings ICALP 89, Stresa, LNCS 372, pages 423–438. Springer-Verlag, 1989.
R. Milner. A Calculus of Communicating Systems. LNCS 92. Springer-Verlag, 1980.
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings Fifth GI Conference, LNCS 104, pages 167–183. Springer-Verlag, 1981.
G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In W. Brauer, editor, Proceedings ICALP 85, Nafplion, LNCS 194, pages 15–32. Springer-Verlag, 1985.
T.C. Przymusinski. On the declarative semantics of deductive databases and logic programs. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 193–216. Morgan Kaufmann Publishers Inc., Los Altos, California, 1987.
R. Reiter. A logic for default reasoning. Artificial Intelligence, 13:81–132, 1980.
F.W. Vaandrager. Algebraic Techniques for Concurrency and their Application. PhD thesis, Centrum voor Wiskunde en Informatica, February 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bol, R., Groote, J.F. (1991). The meaning of negative premises in transition system specifications. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds) Automata, Languages and Programming. ICALP 1991. Lecture Notes in Computer Science, vol 510. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54233-7_157
Download citation
DOI: https://doi.org/10.1007/3-540-54233-7_157
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54233-9
Online ISBN: 978-3-540-47516-3
eBook Packages: Springer Book Archive