Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Deriving Non-determinism from Conjunction and Disjunction
verfasst von : Naijun Zhan, Mila Majster-Cederbaum
Erschienen in: Formal Techniques for Networked and Distributed Systems - FORTE 2005
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we show that the non-deterministic choice “+”, which was proposed as a primitive operator in
Synchronization Tree Logic
(STL for short) can be defined essentially by conjunction and disjunction in the
μ
-calculus (
μ
M for short). This is obtained by extending the
μ
-calculus with the non-deterministic choice “+” (denoted by
μ
M
+
) and then showing that
μ
M
+
can be translated into
μ
M. Furthermore, we also prove that STL can be encoded into
μ
M
+
and therefore into
μ
M.