×
Abadi, Martín; Plotkin, Gordon D.

A logical view of composition. (English) Zbl 0778.68061

Theor. Comput. Sci. 114, No. 1, 3-30 (1993).
We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition rules. The two logics arise naturally from extant specification approaches; one of the logics is intuitionistic, while the other one is linear.
Reviewer: Martín Abadi

Cited in 14 Documents

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Keywords:

compositionality; concurrent programming; modular specification; safety properties; intuitionistic logic; linear logic
PDF BibTeX XML Cite
\textit{M. Abadi} and \textit{G. D. Plotkin}, Theor. Comput. Sci. 114, No. 1, 3--30 (1993; Zbl 0778.68061)
Full Text: DOI

References:

[1] Abadi, M.; Lamport, L., Composing specifications, (Research Report 66 (1990), Digital Equipment Corporation Systems Research Center), a preliminary version appeared in [9]
[2] Abadi, M.; Plotkin, G., A logical view of composition and refinement, Proc. 18th Ann. ACM Symp. on Principles of Programming Languages, 323-332 (1991)
[3] Abrahamson, K., Modal logic of concurrent nondeterministic programs, (Int. Symp. on Semantics of Concurrent Computation (1979), Evian-les-Baines) · Zbl 0402.68010
[4] Abramsky, S., Domain theory in logical form, Ann. Pure Appl. Logic, 51, 1-77 (1991) · Zbl 0737.03006
[5] Abramsky, S.; Vickers, S., Quantales, observational logic, and process semantics (1990), Imperial College, Tech. report · Zbl 0823.06011
[6] Barringer, H.; Kuiper, R.; Pnueli, A., Now you may compose temporal logic specifications, (Proc. 16th Ann. ACM Symp. on Theory of Computing (1984), ACM: ACM New York), 51-63
[7] Dam, M., Relevance logic and concurrent computation, (Proc. 3rd Symp. on Logic in Computer Science (1988), IEEE Press: IEEE Press New York), 178-185
[8] Davey, B. A.; Priestley, H. A., Introduction to Lattices and Order (1991), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0701.06001
[9] (de Bakker, J. W.; de Roever, W.-P.; Rozenberg, G., Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness. Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Lecture Notes in Computer Science, Vol. 430 (1990), Springer: Springer Berlin)
[10] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-134 (1984) · Zbl 0985.68518
[11] Dunn, J. M., Relevance logic and entailment, (Gabbay, D.; Guenthner, F., Handbook of Philosophical Logic, Vol. 3 (1986), Reidel: Reidel Dordrecht), 117-224 · Zbl 0875.03051
[12] Girard, J.-Y., Linear logic, Theoret. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037
[13] Harel, D.; Pnueli, A., On the development of reactive systems, (Apt, K. R., Logics and Models of Concurrent Systems. Logics and Models of Concurrent Systems, NATO ASI Series, Vol. F13 (1984), Springer: Springer Berlin), 477-498 · Zbl 0581.68046
[14] Hennessy, M., Algebraic Theory of Processes (1988), MIT Press: MIT Press Cambridge, MA · Zbl 0744.68047
[15] Hennessy, M.; Plotkin, G., Full abstraction for a simple parallel programming language, (Becvar, J., Proc. 8th Mathematical Foundations of Computer Science Conf.. Proc. 8th Mathematical Foundations of Computer Science Conf., Olomouc, Czechoslovakia. Proc. 8th Mathematical Foundations of Computer Science Conf.. Proc. 8th Mathematical Foundations of Computer Science Conf., Olomouc, Czechoslovakia, Lecture Notes in Computer Science, Vol. 74 (1985), Springer: Springer Berlin) · Zbl 0457.68006
[16] Hennessy, M.; Plotkin, G., Finite conjunctive nondeterminism, (Voss, K.; Genrich, H. J.; Rozenberg, G., Concurrency and Nets (1987), Springer: Springer Berlin), 233-244 · Zbl 0649.03013
[17] Johnstone, P. T., Stone Spaces (1982), Cambridge Univ. Press: Cambridge Univ. Press Cambridge · Zbl 0499.54001
[18] Joyal, A.; Tierney, M., An extension of the Galois theory of Grothendieck, Amer. Math. Soc. Memoirs, 309 (1982)
[19] Lamport, L., Specifying concurrent program modules, ACM Trans. on Programming Languages and Systems, 5, 190-222 (1983) · Zbl 0516.68010
[20] Lamport, L., What good is temporal logic?, (Mason, R. E.A., Information Processing 83: Proc. IFIP 9th World Congr.. Information Processing 83: Proc. IFIP 9th World Congr., Paris (1983), IFIP, North-Holland: IFIP, North-Holland Amsterdam)
[21] Lamport, L., A simple approach to specifying concurrent systems, Commun. ACM, 32, 32-45 (1989)
[22] Martí-Oliet, N.; Meseguer, J., From Petri nets to linear logic, (Tech. Report SRI-CSL-89-4R2 (1989), SRI International) · Zbl 0746.03057
[23] Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Trans. Software Engrg., 417-426 (1981), SE-7 · Zbl 0468.68030
[24] Pnueli, A., In transition from global to modular temporal reasoning about programs, (Apt, K. R., Logics and Models of Concurrent Systems. Logics and Models of Concurrent Systems, NATO ASI Series, Vol. F13 (1984), Springer: Springer Berlin), 123-144
[25] Rosenthal, K. I., Quantales and their Applications, (Pitman Research Notes in Mathematics, Vol. 234 (1990), Longman: Longman Harlow) · Zbl 0703.06007
[26] Stark, E. W., A proof technique for rely/guarantee properties, (Maheshwari, S. N., Foundations of Software Technology and Theoretical Computer Science. Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Vol. 206 (1985), Springer: Springer Berlin), 369-391 · Zbl 0585.68026
[27] Vickers, S., Samson Abramsky on linear process logics, Foundation Workshop Notes (October-November 1988)
[28] Yetter, D. N., Quantales and (noncommutative) linear logic, J. Symbolic Logic, 55, 41-64 (1990) · Zbl 0701.03026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.