×

A unified approach for studying the properties of transition systems. (English) Zbl 0478.68056


MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] de Bakker, J. W., Semantics and termination of non-deterministic recursive programs, 3rd International Colloquium Automata Languages and Programming, 435-477 (1976) · Zbl 0354.68021
[2] Hansen, P. Brinch, Operating Systems Principles (1973), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0308.68007
[3] Clarke, E. M., Synthesis of resource invariants for concurrent programs, ACM Trans. Progr. Languages and Systems, 2, 3, 338-358 (1980) · Zbl 0468.68024
[4] Cousot, P.; Halbwachs, N., Automatic discovery of linear restraints among variables of a program, Proc. 5th ACM Symposium on Principles of Programming Languages, 84-96 (1978), Tuczon, AZ
[5] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, Proc. 6th ACM Symposium on Principles of Programming Languages, 269-282 (1979), San Antonio, TX
[6] Dijkstra, E. W., Solution of a problem in concurrent programming control, Comm. ACM, 8, 9, 569 (1965)
[7] Dijkstra, E. W., Self stabilizing system in spite of distributed control, Comm. ACM, 17, 11, 643-644 (1974) · Zbl 0305.68048
[8] Dijkstra, E. W., Guarded commands, non determinacy and formal derivation of programs, Comm. ACM, 18, 8, 453-457 (1975) · Zbl 0308.68017
[9] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[10] Flon, L.; Suzuki, N., Non determinism and the correctness of parallel programs, (Neuhold, E. J., Formal description of programming concepts (1978), North-Holland: North-Holland Amsterdam), 589-608 · Zbl 0373.68029
[11] Guerreiro, P., A relational model for non-deterministic programs and predicate transformers, (Lecture Notes in Computer Science, 83 (1980), Springer: Springer Berlin), 136-146 · Zbl 0436.68008
[12] Guerreiro, P., Relational semantics of strongly communicating sequential processes, (Research Report No. 200 (1980), IMAG: IMAG Grenoble) · Zbl 0467.68028
[13] Hack, M., Analysis of production schemata by Petri nets (1972), M.I.T, Project MAC
[14] Harel, D., On folk theorems, Comm. ACM, 23, 7, 379-389 (1980) · Zbl 0432.68009
[15] Hoare, C. A.R., Some properties of predicate transformers, JACM, 25, 3, 461-480 (1978) · Zbl 0379.68016
[16] Keller, R. M., Vector replacement systems: a formalism for modeling asynchronous systems, (Technical Report No. 117 (1972), Princeton University)
[17] Keller, R. M., Formal verification of parallel programs, Comm. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[18] Kwong, Y. S., On reduction of asynchronous systems, Theoret. Comput. Sci., 5, 25-50 (1977) · Zbl 0365.68022
[19] Kwong, Y. S., On the absence of livelocks in parallel programs, (Semantics of Concurrent computation. Semantics of Concurrent computation, Lecture Notes in Computer Science, 70 (1979), Springer: Springer Berlin) · Zbl 0402.68023
[20] van Lamsweerde, A.; Sintzoff, M., Formal derivation of strongly correct parallel programs, (Report R338 (1976), MBLE Research Lab). (Report R338 (1976), MBLE Research Lab), Acta Informat., 12, 1, 1-31 (1979) · Zbl 0389.68012
[21] Lamport, L., ‘Sometime’ is sometimes ‘not never’ —On the temporal logic of programs, Proc. 7th Annual ACM Symposium on Principles of Programming Languages, 174-185 (1980), Las Vegas
[22] Lautenbach, K., Liveness in Petri nets, GMD Internal report (1975), ISF 75-02-1, Bonn
[23] Manna, Z.; Pnueli, A., The modal logic of programs, (Lecture Notes in Computer Science, 71 (1979), Springer: Springer Berlin), 385-406 · Zbl 0404.68011
[24] Mazurkiewicz, A., Proving properties of processes, Algorytmy, XI, 19, 5-22 (1974) · Zbl 0305.68044
[25] Park, D., Fixpoint induction and proofs of program properties, Machine Intelligence 5, 59-78 (1969) · Zbl 0219.68007
[26] Peterson, J. L., Petri-nets, Comput. Surveys ACM, 9, 3, 223-252 (1977) · Zbl 0357.68067
[27] Pnueli, A., The temporal semantics of concurrent programs, (Lecture Notes in Computer Science, 70 (1979), Springer: Springer Berlin), 1-20 · Zbl 0402.68009
[28] Queille, J. P.; Sifakis, J., First European Workshop on Applications and Theory of Petri Nets, Strasbourg. First European Workshop on Applications and Theory of Petri Nets, Strasbourg, Iterative methods for the analysis of Petri nets (1980)
[29] de Roever, W. P., Dijkstra’s predicate transformer, non-determinism, recursion and termination, (MFCS ’76. MFCS ’76, Lecture Notes in Computer Science, 45 (1976), Springer: Springer Berlin), 472-481 · Zbl 0341.68014
[30] Rosen, B. K., Correctness of parallel programs: the Church-Rosser approach, Theoret. Comput. Sci., 2, 183-207 (1976) · Zbl 0364.68006
[31] Sifakis, J., Le contrôle des systèmes asynchrones: concepts, propriétés, analyse statique, (Thèse d’Etat (1979), Université de Grenoble)
[32] Sifakis, J., Deadlocks and livelocks in transition systems, (Lecture Notes in Computer Science, 88 (1980), Springer: Springer Berlin), 587-600 · Zbl 0454.68050
[33] Tarski, A., On the calculus of relations, J. Symbolic Logic, 6, 3, 73-89 (1941) · JFM 67.0973.02
[34] Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math., 5, 285-309 (1955) · Zbl 0064.26004
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.