基于线性时序逻辑的实时系统模型检查

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.     

带有时钟变量的线性时序逻辑与实时系统验证

为了描述实时系统的性质和行为,10多年来,各种不同的时序逻辑,如Timed Computation Tree Logic,Metric Interval Temporal Logic和Real-Time Temporal Logic等相继提出来.这些时序逻辑适于表示实时系统的性质和规范,但不适于表示实时系统的实现模型.这样,在基于时序逻辑的实时系统的研究中,系统的性质和实现通常是用两种不同的语言来表示的.定义了一个带有时钟变量的线性时序逻辑(linear temporal logic with clocks,简称LTLC).它是由Manna和Pnueli提出的线性时序逻辑在实时情况下的一个推广.LTLC既能表示实时系统的性质,又能很方便地表示实时系统的实现.它能在统一的语义框架中表示出从高级的需求规范到低级的实现模型之间的不同抽象层次上的系统描述,并且能用逻辑蕴涵来表示不同抽象层次的系统描述之间的语义一致性.LTLC的这个特点将有助于实时系统的性质验证和实时系统的逐步求精.     

Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

Compositional verification aims at managing the complexity of theverification process by exploiting compositionality of the systemarchitecture. In this paper we explore the use of a temporal epistemiclogic to formalize the process of verification of compositionalmulti-agent systems. The specification of a system, its properties andtheir proofs are of a compositional nature, and are formalized within acompositional temporal logic: Temporal Multi-Epistemic Logic. It isshown that compositional proofs are valid under certain conditions.Moreover, the possibility of incorporating default persistence ofinformation in a system, is explored. A completion operation on aspecific type of temporal theories, temporal completion, is introducedto be able to use classical proof techniques in verification withrespect to non-classical semantics covering default persistence.     

实时系统的形式化验证

实时系统的设计对系统设计人员而言是一个巨大挑战。在缺乏严格的验证环境时 ,要避免设计错误是很困难的。本文将一种带时戳的时序逻辑及用于描述具体实时系统的时间变迁系统编码到 HOL定理证明器中 ,并实现了一个基本的规则策略库 ,从而实现了一个简单的交互式辅助验证环境L RP。实例 Fisher算法的互斥性在 IRP中得到了验证。     

Model Checking Temporal Aspects of Inconsistent Concurrent Systems Based on Paraconsistent Logic

Classical logic cannot be used to effectively reason about concurrent systems with inconsistencies (inconsistencies often occur, especially in the early stage of the development, when large and complex concurrent systems are developed). In this paper, we propose the use of a paraconsistent temporal logic (QCTL) for supporting the verification of temporal properties of such systems even where the consistent model is not available. We introduce a novel notion of paraKripke models, which grasps the paraconsistent character of the entailment relation of QCTL. Furthermore, we explore the methodology of model checking over QCTL, and describe the detailed algorithm of implementing QCTL model checker. In the sequel, a simple example is presented, showing how to exploit the proposed model checking technique to verify the temporal properties of inconsistent concurrent systems.     

基于直觉模糊集的不确定时序逻辑模型

针对现有时序逻辑在描述复杂不确定时间信息方面的局限性,提出了一种基于直觉模糊集的不确定时序逻辑模型。该模型分别定义了离散论域和连续论域下的不确定点时序逻辑、点-时段时序逻辑以及时段时序逻辑的判定公式;引入直觉模糊集的犹豫度参数,使得推理结果更加精确。最后通过实例对两类不确定时间信息进行描述,并对其时序逻辑关系的可能性进行度量。通过分析表明该模型是比较优越的。     

计算机支持的协同工作系统的时序逻辑模型

为了使群体能够协同完成任务,CSCW(computer supported cooperative work)系统不仅要解决各种分布性、处理应用领域的特殊性,而且要提供面向用户的协作支持,从而使其行为异常复杂.然而对系统行为进行形式化的描述是构造软件系统的必经阶段.为了清晰地描述CSCW系统的行为,使其特定性质的验证成为可能,本文在时序逻辑的基础上,建立了CSCW系统行为的抽象描述模型.在此模型中,CSCW系统由分布运行实体和信息对象组成,系统的主要行为表现为用时序逻辑语言XYZ/E描述的实体间的交互.此模型可较好地对系统的分析和构造进行指导.     

基于时序Petri网的联锁逻辑形式建模与验证

时序Petri网结合Petri和时序逻辑的优点,清晰简洁地描述并发系统事件间的时序和因果关系,包括系统的最终性和公平性。文章给出安全苛求系统——车站信号联锁逻辑系统的时序Petri网描述,并使用时序逻辑描述系统状态的时序和因果关系,最后通过分析和验证模型的性质得出系统是正确的。     

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

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

基于时序逻辑的加密协议分析

形式化方法由于其精炼，简洁和无二义性，逐步成为分析加密协议的一条可靠和准确的途径，但是加密协议的形式化分析研究目前还不够深入，至今仍没有统一的加密协议验证体系，针对这一现状，该文从加密协议可能面临的最强大的攻击着手，提出了一种基于时序逻辑的加密协议描述方法，在该模型下，对协议行为，入侵者行为，安全需求等特性的描述均用时序逻辑公式表达，从而利用现有的统一的时空逻辑框架分析密码协议的性质，特别地，作者描述和检测了一个系统入侵者不能用任何代数和逻辑的办法获得消息的实例，通过对比，作者认为该方法具有形式化程度较高的特点。     

LORETO: a tool for reducing state explosion in verification of LOTOS programs

LOTOS is a formal specification language for concurrent and distributed systems. Basic LOTOS is the version of LOTOS without value‐passing. A widely used approach to the verification of temporal properties is model checking. Often, in this approach the formal specification is translated into a labeled transition system on which formulae expressing properties are checked. A problem with this verification technique is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. In this paper we show how, given a set ρ of actions, it is possible to automatically obtain for a Basic LOTOS program a reduced transition system to which only the arcs labeled by actions in ρ belong. The set ρ of actions plays a fundamental role in conjunction with a temporal logic defined by the authors in a previous paper: selective mu‐calculus. The reduced system with respect to ρ preserves the truth value of all selective mu‐calculus formulae with actions from the set ρ. We act at both syntactic and semantic levels. From a syntactic point of view, we define a set of transformation rules obtaining a smaller program. On the semantic side, we define a non‐standard semantics which dynamically reduces the transition system during generation. We present a tool implementing both the syntactic and the semantic reduction. Copyright © 1999 John Wiley & Sons, Ltd.     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为，10多年来，各种时序逻辑，如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范，但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic，简称HPTL），既能刻画混合系统的性质，又能表示混合系统的实现。这样，混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时，给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。     

Model‐Based Visualization of Temporal Abstractions

We describe a new conceptual methodology and related computational architecture called Knowledge‐based Navigation of Abstractions for Visualization and Explanation (KNAVE). KNAVE is a domain‐independent framework specific to the task of interpretation, summarization, visualization, explanation, and interactive exploration, in a context‐sensitive manner, of time‐oriented raw data and the multiple levels of higher level, interval‐based concepts that can be abstracted from these data. The KNAVE domain‐independent exploration operators are based on the relations defined in the knowledge‐based temporal‐abstraction problem‐solving method, which is used to abstract the data, and thus can directly use the domain‐specific knowledge base on which that method relies. Thus, the domain‐specific semantics are driving the domain‐independent visualization and exploration processes, and the data are viewed through a filter of domain‐specific knowledge. By accessing the domain‐specific temporal‐abstraction knowledge base and the domain‐specific time‐oriented database, the KNAVE modules enable users to query for domain‐specific temporal abstractions and to change the focus of the visualization, thus reusing for a different task (visualization and exploration) the same domain model acquired for abstraction purposes. We focus here on the methodology, but also describe a preliminary evaluation of the KNAVE prototype in a medical domain. Our experiment incorporated seven users, a large medical patient record, and three complex temporal queries, typical of guideline‐based care, that the users were required to answer and/or explore. The results of the preliminary experiment have been encouraging. The new methodology has potentially broad implications for planning, monitoring, explaining, and interactive data mining of time‐oriented data.     

Symmetry and model checking

We show how to exploit symmetry in model checking for concurrent systems containing many identical or isomorphic components. We focus in particular on those composed of many isomorphic processes. In many cases we are able to obtain significant, even exponential, savings in the complexity of model checking.The author's work was supported in part by NSF Grant CCR 941-5496, Semiconductor Research Corporation Contract 95-DP-388, and Texas Advanced Technology Program Grant 003658-250.The author's work was supported in part by NSF Grant CCR-9212183.     

Reasoning in Medical and Tutoring Systems: A Decidable First-Order Temporal Paraconsistent Non-Commutative Logic

Reasoning in medical and tutoring systems requires expressions relating not only to time-dependency, paraconsistency, constructiveness, and resource-sensitivity, but also order-sensitivity. Our objective in this study is to construct a decidable rst-order logic for appropriately expressing this reasoning. To meet this objective, we introduce a rst-order temporal paraconsistent non-commutative logic as a Gentzen-type sequent calculus. This logic has no structural rules but has some bounded temporal operators and a paraconsistent negation connective. The main result of this study is to show this logic to be decidable. Based on this logic, we present some illustrative examples for reasoning in medical and tutoring systems.     

基于状态可达图的离散事件系统时态性质分析

离散事件系统的许多重要性质可用时态逻辑方便，直接和简明地进行描述，系统的性质分析可转化成时态满足关系的判定。基于状态可达图，给出了有限系统时态特征的判定方法。     

基于时序逻辑的面向实现的协议规范语言

在多种形式化描述语言和时序逻辑原理的研究之上；针对通讯协议的特点提出一个协议模型思想，并设计了实现此模型协议描述语言．本方法的特点是：基于时序逻辑；引入了面向对象的概念，对事件有强的描述能力，让描述更接近于现实；扩展了对事件的描述．能描述事件的随机发生，我们已将之成功地应用于对超文本协议的描述．     

An Interpretation of Default Logic in Minimal Temporal Epistemic Logic

When reasoning about complex domains, where information available is usually only partial, nonmonotonic reasoning can be an important tool. One of the formalisms introduced in this area is Reiter's Default Logic (1980). A characteristic of this formalism is that the applicability of default (inference) rules can only be verified in the future of the reasoning process. We describe an interpretation of default logic in temporal epistemic logic which makes this characteristic explicit. It is shown that this interpretation yields a semantics for default logic based on temporal epistemic models. A comparison between the various semantics for default logic will show the differences and similarities of these approaches and ours.