×

zbMATH — the first resource for mathematics

A logical view of composition. (English) Zbl 0778.68061
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

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Lamport, L., Composing specifications, (), 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, () · 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, (), 51-63
[7] Dam, M., Relevance logic and concurrent computation, (), 178-185
[8] Davey, B.A.; Priestley, H.A., Introduction to lattices and order, (1991), Cambridge University Press Cambridge · Zbl 0701.06001
[9] ()
[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, (), 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, (), 477-498 · Zbl 0581.68046
[14] Hennessy, M., Algebraic theory of processes, (1988), MIT Press Cambridge, MA · Zbl 0744.68047
[15] Hennessy, M.; Plotkin, G., Full abstraction for a simple parallel programming language, () · Zbl 0457.68006
[16] Hennessy, M.; Plotkin, G., Finite conjunctive nondeterminism, (), 233-244 · Zbl 0649.03013
[17] Johnstone, P.T., Stone spaces, (1982), 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?, ()
[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, () · 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, (), 123-144
[25] Rosenthal, K.I., Quantales and their applications, () · Zbl 0703.06007
[26] Stark, E.W., A proof technique for rely/guarantee properties, (), 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.