×

From synchronization tree logic to acceptance model logic. (English) Zbl 0572.68020

Logics of programs, Proc. Conf., Brooklyn/N.Y. 1985, Lect. Notes Comput. Sci. 193, 128-142 (1985).
[For the entire collection see Zbl 0562.00009.]
A logic called Acceptance Model Logic (AML) is presented. Its language of formulas contains a subset of TCSP terms. The subset of TCSP considered, is the term language generated from the constants Chaos and Stop by using unary action operators \(a\in A\) and the binary internal and external non- deterministic choice operators. We study the relationship of AML with synchronization Tree Logic (STL), defined in a preceding paper. A Galois connection is defined between the classes of models of the two logics. This allows us to obtain a sound and complete axiomatization of AML by adding some axioms to the axiomatization of STL.

MSC:

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
03B60 Other nonclassical logic
03C52 Properties of classes of models

Citations:

Zbl 0562.00009