Model-checking dense-time Duration Calculus

Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics.The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones     

From Discrete Duration Calculus to Symbolic Automata

The goal of this paper is to translate (fragments of) the quantified discrete duration calculus QDDC, proposed by P. Pandya, into symbolic acceptors with counters. Acceptors are written in the synchronous programming language Lustre, in order to allow available symbolic verification tools (model-checkers, abstract interpreters) to be applied to properties expressed in QDDC. We show that important constructs of QDDC need non-deterministic acceptors, in order to be translated with a bounded number of counters, and an expressive fragment of the logic is identified and translated. Then, we consider a more restricted fragment, which only needs deterministic acceptors.     

Decidability of a Hybrid Duration Calculus

We present a logic which we call Hybrid Duration Calculus (HDC). HDC is obtained by adding the following hybrid logical machinery to the Restricted Duration Calculus (RDC): nominals, satisfaction operators, down-arrow binder, and the global modality. RDC is known to be decidable, and in this paper we show that decidability is retained when adding the hybrid logical machinery. Decidability of HDC is shown by reducing the satisfiability problem to satisfiability of Monadic Second-Order Theory of Order. We illustrate the increased expressive power obtained in hybridizing RDC by showing that HDC, in contrast to RDC, can express all of the 13 possible relations between intervals.     

Duration calculus: Logical foundations

The Duration Calculus (abbreviated DC) represents a logical approach for formal design of real-time systems, where real numbers are used to model time and Boolean valued functions over time are used to model states and events of real-time systems. Since its introduction, DC has been applied to many case studies and it has been extended in several directions. The aim of this paper is to provide a thorough presentation of the logic.on leave of absence from Software Institute, Academia Sinica, Beijing     

Probabilistic Duration Calculus for Continuous Time

This paper deals with dependability of imperfect implementations concerning given requirements. The requirements are assumed to be written as formulas in Duration Calculus. Implementations are modelled by continuous semi-Markov processes with finite state space, which are expressed in the paper as finite automata with stochastic delays of state transitions. A probabilistic model for Duration Calculus formulas is introduced, so that the satisfaction probabilities of Duration Calculus formulas with respect to semi-Markov processes can be defined, reasoned about and calculated through a set of axioms and rules of the model. Received November 1994 / Accepted in revised form June 1998     

On the completeness of the Lambek Calculus with respect to relativized Relational Semantics

Recently M. Szabolcs [12] has shown that many substructural logics including Lambek CalculusL are complete with respect to relativized Relational Semantics. The current paper proves that it is sufficient forL to consider a relativization to the relation x dividesy in some fixed semigroupG.Research partially supported by the Russian Fund for Fundamental Research Grant 93-012-590.     

一类混合系统稳态型仿真时间的确定方法

对于随机性混合系统稳态型仿真,其仿真时间的确定方法是一个值得研究的问题。该文以线性跳变系统为例,研究了一类混合系统稳态型仿真时间的优化准则与计算方法,并给出了应用实例。     

计算智能融合应用研究

本文对神经网络（NN），进化算法（EA0，不确定理论（Uncertain Theory）混沌系统（Chaos System）、免疫算法（IA,Immune Algorithm）、DNA计算（DNA Coputing）等广义计算智能相互融合应用进行了总结和分析，重点介绍免疫算法、DNA计算等新型计算智能理论的相互融合应用，最后对计算智能理论的融合应用趋势进行探讨。     

Comparing model checking and logical reasoning for real-time systems

We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is used to verify the correctness of the protocol by logical reasoning. An alternative but consistent operational semantics in terms of Timed Automata is used to verify the correctness by model checkers. Since model checking of the full model does not terminate in all cases within an acceptable time we examine abstractions and their influence on model-checking performance. We present two abstraction methods that can be applied successfully for the protocol presented.Received June 1999Accepted in revised form September 2003 by M.R. Hansen and C. B. Jones     

混合系统的建模设计与仿真综述

混合系统是一类既包含连续动态行为又包含离散动态行为的系统,这类系统在实际应用中显得越来越重要,对这类系统需要探索新的模型和研究方法。该文在概述混合系统概念、特点以及发展近况的基础上,主要综述了近年来混合系统研究中的一些重要问题,指出现有各种方法的优缺点,并指出了今后的研究方向。该文首先介绍了混合系统研究中多种常见的建模方法,如混合自动机、Petri网和时段演算,然后重点讨论了混合系统一些重要性质,主要集中在对系统稳定性、可达性、可观性的分析方法上,以及混合系统的多种设计方法,并且对这些方法进行了初步评价,最后介绍了混合系统研究中一些常用的仿真工具。