A new algebraic semantic approach and some adequate connectives for computation with temporal logic over discrete time
作者:
Alfredo Burrieza,
InmaP. de Guzmán,
期刊:
Journal of Applied Non-Classical Logics
(Taylor Available online 1992)
卷期:
Volume 2,
issue 2
页码: 181-200
ISSN:1166-3081
年代: 1992
DOI:10.1080/11663081.1992.10510781
出版商: Taylor & Francis Group
数据来源: Taylor
摘要:
In this paper we present a new semantic approach for propositional linear temporal logic with discrete time, strongly based in the well-order of IN (the set of natural numbers). We consider temporal connectives which express precedence, posteriority and simultaneity, and they provide a family of expressively complete temporal logics. The selection of the new semantics and connectives used in this work was principally to obtain a suitable executable temporal logic, which can be used for the specification and control of process behaviour in discrete time in a similar way to thai presented by D. Gabbay in [GAB 89], Our new approach has two advantages: firstly, the connectives are defined intuitively so that they have interpretations which relate to properties of interest in real systems; secondly, it provides a new semantics that facilitates simpler proofs of many valid formulas and metatheorems. To confirm this second advantage, we use our semantics to give a formal proof of the Separation Theorem for one of these logics (specifically LN3). The great interest of this Separation Theorem for the executable temporal logic is emphasised by D. Gabbay in [GAB 89], [GAB 88].
点击下载:
PDF (684KB)
返 回