从活性顺序图到时态逻辑的转化方法

为了将活性顺序图用于模型检测,方便描述系统的场景需求,提出了一种将活性顺序图转换成时态逻辑的转化方法.分析活性顺序图语言并且定义一种基于路径的语义,用活性顺序图表述系统的场景需求.根据提出的语义,给出了一个将场景需求显式转化为时态逻辑的一般方法,针对并发消息较多的系统扩展和优化此方法,以得到更简短的时态逻辑公式.通过实例说明活性顺序图到线性时态逻辑的转化过程.     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

Alternating-time stream logic for multi-agent systems

Constraint automata have been introduced to provide a uniform operational model for specifying service interfaces of components, the network that yields the glue code for the components, and the operational behavior of the composite system. Constraint automata have been used as the basis for equivalence checking and model checking temporal logical properties. This paper presents a multi-player semantics for constraint automata which serves to reason about controllability, interaction and cooperation facilities of individual components or coalitions of components in a given network. We introduce a temporal logic framework, called alternating-time stream logic, that combines classical features of alternating-time logic (ATL) for concurrent games with special operators for specifying regular conditions on the data streams in the network and on the write and read operations at the I/O-ports of the components. Since constraint automata support any kind of synchronous and asynchronous peer-to-peer communication, the resulting game structure is non-standard and requires a series of nontrivial adaptations to the semantics and verification algorithms for classical alternating-time approaches.     

Temporal inferencing on administrative databases

Temporal inferencing is basic to business data processing, e.g. in such concepts as income, wealth, exchange, budgeting and contractual commitment. Time appears in numerous forms within the information system, however, in data items of varying syntax; or implicitly, in the current state of the database. Here, a uniform concept of time based on temporal intervals over a continuous calendar scale is suggested for administrative applications. Temporal operators and related axioms are proposed for logical databases.     

ON TEMPORAL DEDUCTIVE DATABASES

This article introduces a temporal deductive database system featuring a logic programming language and an algebraic front-end. The language, called Temporal DATALOG, is an extension of DATALOG based on a linear-time temporal logic in which the flow of time is modeled by the set of natural numbers. Programs of Temporal DATALOG are considered as temporal deductive databases, specifying temporal relationships among data and providing base relations to the algebraic front-end. The minimum model of a given Temporal DATALOG program is regarded as the temporal database the program models intensionally. The algebraic front-end, called TRA, is a point-wise extension of the relational algebra upon the set of natural numbers. When needed during the evaluation of TRA expressions, slices of temporal relations over intervals can be retrieved from a given temporal deductive database by bottom-up evaluation strategies.
A modular extension of Temporal DATALOG is also proposed, through which temporal relations created during the evaluation of TRA expressions may be fed back to the deductive part for further manipulation. Modules therefore enable the algebra to have full access to the deductive capabilities of Temporal DATALOG and to extend it with nonstandard algebraic operators. This article also shows that the temporal operators of TRA can be simulated in Temporal DATALOG by program clauses.     

符号化模型检测CTL

提出了一个关于时态逻辑CTL＊ 的符号化模型检测算法.该算法通过所谓的tableau构造方法来判定一个有限状态系统是否满足CTL＊规范. 根据该理论,作者已实现了一个基于OBDD技术的CTL＊符号化模型检测工具MCTK,并完成了相当数量的实验.到目前为止,已知有名的符号化模型检测工具,如SMV和NuSMV等, 都只能对CTL＊的子集逻辑（如CTL,LTL）进行检测,而文中算法的结果是令人满意的,并且当规范不是特别复杂时, 高效的CTL＊符号化模型检测是可能的.     

Probabilistic Belief Logic and Its Probabilistic Aumann Semantics

In this paper, we present a logic system for probabilistic belief named PBL,which expands the language of belief logic by introducing probabilistic belief. Furthermore, we give the probabilistic Aumann semantics of PBL. We also list some valid properties of belief and probabilistic belief, which form the deduction system of PBL. Finally, we prove the soundness and completeness of these properties with respect to probabilistic Aumann semantics.     

Symmetric structure in logic programming

It is argued that some symmetric structure in logic programs could be taken into account when implementing semantics in logic programming. This may enhance the declarative ability or expressive power of the semantics. The work presented here may be seen as representative examples along this line. The focus is on the derivation of negative information and some other classic semantic issues. We first define a permutation group associated with a given logic program. Since usually the canonical models used to reflect the common sense or intended meaning are minimal or completed models of the program, we expose the relationships between minimal models and completed models of the original program and its so-called G-reduced form newly-derived via the permutation group defined. By means of this G-reduced form, we introduce a rule to assume negative information termed G-CWA, which is actually a generalization of the GCWA. We also develop the notions of G-definite, G-hierarchical and G-stratified logic programs,     

多智体系统时序认知规范的SPIN模型检测

SPIN模型检测器主要用来检测线性时序逻辑描述的规范,而多智体系统的规范采用时序认知逻辑描述比较方便。本文着重讨论了如何利用SPIN模型检测线性时序认知逻辑的方法,根据局部命题的理论,将模型检测知识算子和公共算子表述的规范规约为模型检测线性时序逻辑的问题,从而使SPIN的检测功能由线性时序逻辑扩充到线性时序认知逻辑。本文通过一个RPC协议分析实例来说明模型检测线性时序认知逻辑的方法。     

A temporal programming model with atomic blocks based on projection temporal logic

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model （αPTL） which extends the projection temporal logic （PTL） to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.     

A logic programming system for nonmonotonic reasoning

The evolution of logic programming semantics has included the introduction of a new explicit form of negation, beside the older implicit (or default) negation typical of logic programming. The richer language has been shown adequate for a spate of knowledge representation and reasoning forms.The widespread use of such extended programs requires the definition of a correct top-down querying mechanism, much as for Prolog wrt. normal programs. One purpose of this paper is to present and exploit a SLDNF-like derivation procedure, SLX, for programs with explicit negation under well-founded semantics (WFSX) and prove its soundness and completeness. (Its soundness wrt. the answer-sets semantics is also shown.) Our choice ofWFSX as the base semantics is justi-fied by the structural properties it enjoys, which are paramount for top-down query evaluation.Of course, introducing explicit negation requires dealing with contradiction. Consequently, we allow for contradiction to appear, and show moreover how it can be removed by freely changing the truth-values of some subset of a set of predefined revisable literals. To achieve this, we introduce a paraconsistent version ofWFSX, WFSX _p , that allows contradictions and for which our SLX top-down procedure is proven correct as well.This procedure can be used to detect the existence of pairs of complementary literals inWESX _p simply by detecting the violation of integrity rulesf L, -L introduced for eachL in the language of the program. Furthermore, integrity constraints of a more general form are allowed, whose violation can likewise be detected by SLX.Removal of contradiction or integrity violation is accomplished by a variant of the SLX procedure that collects, in a formula, the alternative combinations of revisable literals' truth-values that ensure the said removal. The formulas, after simplification, can then be satisfied by a number of truth-values changes in the revisable, among true, false, and undefined. A notion of minimal change is defined as well that establishes a closeness relation between a program and its revisions. Forthwith, the changes can be enforced by introducing or deleting program rules for the revisable literals.To illustrate the usefulness and originality of our framework, we applied it to obtain a novel logic programming approach, and results, in declarative debugging and model-based diagnosis problems.     

有界模型检测同步多智体系统的时态认知逻辑

提出在同步的多智体系统中验证时态认知逻辑的有界模型检测(bounded model checking,简称BMC)算法.基于同步解释系统语义,在时态逻辑CTL*的语言中引入认知模态词,从而得到一个新的时态认知逻辑ECKL_n.通过引入状态位置函数的方法获得同步系统的智能体知识,避免了为时间域而扩展通常的时态认知模型的状态及迁移关系编码.ECKL_n的时态认知表达能力强于另一个逻辑CTLK.给出该算法的技术细节及正确性证明,并用火车控制系统实例解释算法的执行过程.     

时态认知逻辑CTL＊K的符号化模型检查算法

时序认知逻辑是由时序逻辑和认知逻辑组合而成的逻辑,主要应用于多主体系统的规范定义.大多数时序认知逻辑是基于CTL的,表达能力有限.并且已知的一些模型检查算法存在内存不足和状态爆炸等问题.讨论了基于CTL*的时态认知逻辑cTL*K的语法、语义和模型,它能够在表达力很强的时态逻辑CTL*基础上描述智能体的知识、目标等意向特征.并给出了CTL*K的模型检查算法,其核心思想就是将CTL*K公式的检查问题转化为CTL*公式的模型检查问题,可以使检查的系统规模得以大幅度提高.并且将算法编码后容易集成到NuSMV模型检查器.     

Syntax and Semantics for a Fuzzy Temporal Constraint Logic

In this paper we establish the relationship between the syntax and semantics of a fuzzy temporal constraint logic (FTCL) proposed by Cárdenas et al. FTCL enables us to express interrelated events by means of fuzzy temporal constraints. Moreover, it provides a resolution principle for performing inferences which take these constraints into account. FTCL is compatible with the theoretical temporal reasoning model proposed by Marín et al. – the Fuzzy Temporal Constraint Networks (FTCN). The main contributions of this paper are, on the one hand, the proofs of the FTCL-deduction and the FTCL-refutation theorems, and, on the other, the proof of the soundness of the refutation by resolution in this formal system, together with an exhaustive study of its completeness.     

Adding a temporal dimension to a logic system

We introduce a methodology whereby an arbitrary logic system L can be enriched with temporal features to create a new system T(L). The new system is constructed by combining L with a pure propositional temporal logic T (such as linear temporal logic with Since and Until) in a special way. We refer to this method as adding a temporal dimension to L or just temporalising L. We show that the logic system T(L) preserves several properties of the original temporal logic like soundness, completeness, decidability, conservativeness and separation over linear flows of time. We then focus on the temporalisation of first-order logic, and a comparison is make with other first-order approaches to the handling of time.     

Completeness of a combination of neighbourhood logic and temporal logic

This paper presents a completeness result, with respect to a possible world semantics, for a combination of a first-order temporal logic and neighbourhood logic. This logic was considered by Qiu and Zhou (1998, Proceedings of the PROCOMET 98, pp 444–461) to define semantics of a real-time OCCAM-like programming language.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones     

A temporal programming model with atomic blocks based on projection temporal logic

Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model (αPTL) which extends the projection temporal logic (PTL) to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.     

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.     

模糊交互时态逻辑的模型检测

交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题。首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性。然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析。     

Class Based Contextual Logic for DOOD

Cntextual logic provides a mechanism to reason about modules.In this paper,this theory of modules if modules is extended to a context theory of classes where class is in the true spirit of object-oriented databases.The logic,referred to as CLOG,is class-based.CLOG supports class,object identity,multiple role of object, monotonic and non-monotonic inheritance of data and method,method factoring,views,derived and query classes.Views and derived classes are queries in themselves.Objects are pure data terms representing the ground instances of facts in the class.Object identity is a first class term in the logic.Inheritance is handled through delegation.