Der Artikel untersucht eine Verallgemeinerung des Kirchensynthese-Problems auf die kontinuierliche Zeit der nicht-negativen reellen Zahlen. Es zeigt sich, dass es in der kontinuierlichen Zeit Phänomene gibt, die sich sehr von der kanonischen diskreten Zeitdomäne der natürlichen Zahlen unterscheiden.
Im Einzelnen:
Das Kirchensyntheseproblem in der kontinuierlichen Zeit ist indeterminiert. Es gibt MSO[<]-Formeln Ψ(X, Y), für die es weder einen kausalitätserhaltenden (C-) Operator F mit FVsig |= ∀X. Ψ(X, F(X)) noch einen stark kausalitätserhaltenden (SC-) Operator G mit FVsig |= ∀Y. ¬Ψ(G(Y), Y) gibt.
Das Dichotomie-Theorem aus dem diskreten Fall gilt nicht. Es gibt MSO[<]-Formeln Ψ(X, Y), für die es sowohl einen C-Operator F mit FVsig |= ∀X. Ψ(X, F(X)) als auch einen SC-Operator G mit FVsig |= ∀Y. ¬Ψ(G(Y), Y) gibt.
Es gibt MSO[<]-Formeln Ψ(X, Y), die zwar durch einen C-Operator implementiert werden können, aber nicht durch einen MSO[<]-definierbaren C-Operator.
Trotz dieser Unterschiede zur diskreten Zeit zeigt der Artikel, dass das Kirchensyntheseproblem in der kontinuierlichen Zeit entscheidbar ist. Es wird ein Algorithmus präsentiert, der für eine gegebene MSO[<]-Formel Ψ(X, Y) entscheidet, ob es einen MSO[<]-definierbaren C-Operator gibt, der Ψ implementiert, und falls ja, einen solchen Operator konstruiert.
他の言語に翻訳
原文コンテンツから
arxiv.org
深掘り質問