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

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

Clausal resolution in a logic of rational agency

A resolution based proof system for a Temporal Logic of Possible Belief is presented. This logic is the combination of the branching-time temporal logic CTL (representing change over time) with the modal logic KD45 (representing belief ). Such combinations of temporal or dynamic logics and modal logics are useful for specifying complex properties of multi-agent systems. Proof methods are important for developing verification techniques for these complex multi-modal logics. Soundness, completeness and termination of the proof method are shown and simple examples illustrating its use are given.     

A framework for multi-robot motion planning from temporal logic specifications

We propose a framework for the coordination of a network of robots with respect to formal requirement specifications expressed in temporal logics.A regular tessellation is used to partition the space of interest into a union of disjoint regular and equal cells with finite facets,and each cell can only be occupied by a robot or an obstacle.Each robot is assumed to be equipped with a finite collection of continuous-time nonlinear closed-loop dynamics to be operated in.The robot is then modeled as a hybrid automaton for capturing the finitely many modes of operation for either staying within the current cell or reaching an adjacent cell through the corresponding facet.By taking the motion capabilities into account,a bisimilar discrete abstraction of the hybrid automaton can be constructed.Having the two systems bisimilar,all properties that are expressible in temporal logics such as Linear-time Temporal Logic,Computation Tree Logic,and μ -calculus can be preserved.Motion planning can then be performed at a discrete level by considering the parallel composition of discrete abstractions of the robots with a requirement specification given in a suitable temporal logic.The bisimilarity ensures that the discrete planning solutions are executable by the robots.For demonstration purpose,a finite automaton is used as the abstraction and the requirement specification is expressed in Computation Tree Logic.The model checker Cadence SMV is used to generate coordinated verified motion planning solutions.Two autonomous aerial robots are used to demonstrate how the proposed framework may be applied to solve coordinated motion planning problems.     

计算树逻辑特性模式研究

模型检查是系统验证的有效方法,在验证过程中需要对系统待检验特性用时态逻辑公式进行刻画,然后在模型检查工具中进行检验。介绍计算树逻辑的语法及语义,根据计算树逻辑中特性模式的划分及作用范围给出计算树逻辑常见的特性模式,包括缺失性模式、存在性模式、普遍性模式、优先性模式和跟随性模式等。     

Quantified Computation Tree Logic

Computation Tree Logic (CTL) is one of the most syntactically elegant and computationally attractive temporal logics for branching time model checking. In this paper, we observe that while CTL can be verified in time polynomial in the size of the state space times the length of the formula, there is a large set of reachability properties which cannot be expressed in CTL, but can still be verified in polynomial time. We present a powerful extension of CTL with first-order quantification over sets of reachable states. The extended logic, QCTL, preserves the syntactic elegance of CTL while enhancing its expressive power significantly. We show that QCTL model checking is PSPACE-complete in general, but has a rich fragment (containing CTL) which can be checked in polynomial time. We show that this fragment is significantly more expressive than CTL while preserving the syntactic beauty of CTL.     

TCTL Inevitability Analysis of Dense-Time Systems: From Theory to Engineering

Inevitability properties in branching temporal logics are of the syntax foralldiamondsuit phi, where phi is an arbitrary (timed) CTL (Computation Tree Logic) formula. Such inevitability properties in dense-time logics can be analyzed with the greatest fixpoint calculation. We present algorithms to model-check inevitability properties. We discuss a technique for early decision on greatest fixpoint calculation which has shown promising performance against several benchmarks. We have experimented with various issues which may affect the performance of TCTL inevitability analysis. Specifically, our algorithms come with a parameter for the measurement of time-progress. We report the performance of our implementation with regard to various parameter values and with or without the non-Zeno computation requirement in the evaluation of greatest fixpoints. We have also experimented with safe abstraction techniques for model-checking TCTL inevitability properties. The experiment results help us in deducing rules for setting the parameter for verification performance. Finally, we summarize suggestions for configurations of efficient TCTL inevitability evaluation procedure.     

A Model Checking-based Method for Verifying Web Application Design

Development of Web Applications (WA) needs new methods, techniques and tools to support an engineered project during all the phases of its life cycle. To ensure the reliability of WA it is important they be validated and verified at early design phase. We use Model Checking techniques to perform automated verification of the UML design of a WA.We propose a mathematical model of a WA partitioning the usual Kripke structure into windows, links, pages and actions. Then we specify properties to be checked in a temporal logic, Computation Tree Logic (CTL). Verification is performed adapting the SMV model checker to our formalism. An implemented system that embeds the SMV verifier automatically parses the XMI output of UML tool and builds the SMV model to be verified with respect to specifications. Results of verification proved the benefits of the method.     

RGITL: A temporal logic framework for compositional reasoning about interleaved programs

This paper gives a self-contained presentation of the temporal logic Rely-Guarantee Interval Temporal Logic (RGITL). The logic is based on interval temporal logic (ITL) and higher-order logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles of symbolic execution and induction, known from the verification of sequential programs, which are transferred to a concurrent setting with temporal logic. We include an interleaving operator with compositional semantics. As a consequence, the calculus permits proving decomposition theorems which reduce reasoning about an interleaved program to reasoning about individual threads. A central instance of such theorems are rely-guarantee (RG) rules, which decompose global safety properties. We show how the correctness of such rules can be formally derived in the calculus. Decomposition theorems for other global properties are also derivable, as we show for the important progress property of lock-freedom. RGITL is implemented in the interactive verification environment KIV. It has been used to mechanize various proofs of concurrent algorithms, mainly in the area oflinearizable and lock-free algorithms.     

强弱例外下的交互时态逻辑

非单调推理是众多人工智能应用系统都可能面对的问题,多Agent系统也不例外。在前期关于Agent BDI逻辑、多Agent合作逻辑、多Agent合作问题求解过程建模等研究工作的基础上,借鉴Baral等人开发非单调线性时态逻辑N-LTL的技术,利用强弱例外对多Agent合作逻辑的开创性工作交互时态逻辑(ATL)进行拓展,建立非单调交互时态逻辑NATL,给出其语法和语义。是对ATL进行非单调拓展的首次有益尝试。可以考虑以之为理论工具对多Agent思维状态及其动态修正机制进行妥善刻画。     

Abstraction and approximation in fuzzy temporal logics and models

Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic* (FzCTL*). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models.     

First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).     

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

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

Reasoning in a Restricted Temporal Logic

We consider RTL, a linear time propositional temporal logic whose only modalities are the [formula] (eventually) operator and its dual [formula] (always). Although less expressive than the full temporal logic, RTL is the fragment of temporal logic that is used most often and in many verification systems. Indeed, many properties of distributed systems discussed in the literature are RTL properties. Another advantage of RTL over the full temporal logic is in the decidability procedure; while deciding satisfiability of a formula in full temporal logic is a PSPACE complete procedure, doing so for an RTL formula is in NP. We characterize the class of ω-regular languages that are definable in RTL and show simple translations between ω-regular sets and RTL formulae that define them. We explore the applications of RTL in reasoning about communication systems. Finally, we relate variants of RTL (when interpreted over a real line segments) to several fragments of Interval Modal Logic and show that the satisfiability problem for RTL when interpreted over a real line is NP-complete.     

A Dynamic Logic of Agency I: STIT,Capabilities and Powers

The aim of this paper, is to provide a logical framework for reasoning about actions, agency, and powers of agents and coalitions in game-like multi-agent systems. First we define our basic Dynamic Logic of Agency (DLA{\mathcal{DLA}}). Differently from other logics of individual and coalitional capability such as Alternating-time Temporal Logic (ATL) and Coalition Logic, in DLA{\mathcal{DLA}} cooperation modalities for expressing powers of agents and coalitions are not primitive, but are defined from more basic dynamic logic operators of action and (historic) necessity. We show that STIT logic can be reconstructed in DLA{\mathcal{DLA}}. We then extend DLA{\mathcal{DLA}} with epistemic operators, which allows us to distinguish capability and power. We finally characterize the conditions under which agents are aware of their capabilities and powers.     

A Formalism for Representing and Reasoning with Temporal Information,Event and Change

In this paper we present a general formalism for representing and reasoning with temporal information, event and change. The temporal framework is a theory of time that takes both points and interval as temporal primitives and where the base logic is that of Kleene’s three-valued logic. Thus, we can avoid the Divided Instant Problem (DIP). We present a three-valued based Temporal First-Order Nonmonotonic Logic (TFONL) that employs an explicit representation of time and events. We may embody default logic into TFONL, which takes into consideration the frame, qualification and ramification problems.     

CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks

Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for genetic regulatory networks (Grns). Applications of model checking in systems biology have revealed that temporal logics should be able to capture both branching-time and fairness properties (needed for specifying multistability and oscillation properties, respectively). At the same time, they should have a user-friendly syntax easy to employ by non-experts. In this paper, we define Computation Tree Regular Logic (Ctrl), an extension of Ctl with regular expressions and fairness operators that attempts to match these criteria. Ctrl subsumes both Ctl and Ltl, and has a reduced set of temporal operators indexed by regular expressions. We also develop a translation of Ctrl into Hennessy-Milner Logic with Recursion (HmlR), an equational variant of the modal μ-calculus. This has allowed us to obtain an on-the-fly model checker with diagnostic for Ctrl by directly reusing the verification technology available in the Cadp toolbox. We illustrate the application of the Ctrl model checker by analyzing the Grn controlling the carbon starvation response of Escherichia coli.     

基于χChek的软件产品线多值模型检测方法

软件产品线保持产品个性化的同时提高了公共部分的复用。但软件产品线中包含的不确定信息,给产品带来了潜在风险。形式化验证技术逐步应用于软件产品线验证。但是传统的布尔逻辑模型不能很好地描述软件产品线的不确定性和不一致性。本文结合多值模型检测器χChek,通过基于动作的模型描述方法,对软件产品线进行描述,然后转换成为χChek规定的模型格式,同时提供多值逻辑描述。最后采用计算树逻辑描述产品线属性,使用χChek进行验证。     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

Invariant-Free Clausal Temporal Resolution

Resolution is a well-known proof method for classical logics that is well suited for mechanization. The most fruitful approach in the literature on temporal logic, which was started with the seminal paper of M. Fisher, deals with Propositional Linear-time Temporal Logic (PLTL) and requires to generate invariants for performing resolution on eventualities. The methods and techniques developed in that approach have also been successfully adapted in order to obtain a clausal resolution method for Computation Tree Logic (CTL), but invariant handling seems to be a handicap for further extension to more general branching temporal logics. In this paper, we present a new approach to applying resolution to PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Hence, we say that the approach presented in this paper is invariant-free. Our method is based on the dual methods of tableaux and sequents for PLTL that we presented in a previous paper. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called trs-resolution, that extends classical propositional resolution. Finally, we prove that trs-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL.