一种基于时间自动机的时钟等价性优化方法

提出了一种优化模型检验时间自动机的时钟等价规则,通过优化的时钟等价规则,使时间自动机等价后的域自动机状态数尽可能少,并在此基础上定义了适合于优化时钟等价规则的域自动机.优化时钟等价规则,在一定程度上有效地解决了状态空间爆炸问题.     

Timed Property Sequence Chart

Property Sequence Chart (PSC) is a novel scenario-based notation, which has been recently proposed to represent temporal properties of concurrent systems. This language balances expressive power and simplicity of use. However, the current version of PSC just represents the order of events and lacks the ability to express timing properties. In real-time systems, it is well known that these timing requirements are very important and need to be specified clearly. Thus, in this paper, we define timed PSC (TPSC) and give the semantics of TPSC in terms of Timed Büchi Automaton (TBA). Then, we measure the expressive power of TPSC based on the recently proposed real-time specification patterns. Finally, we illustrate the use of TPSC in the context of a web service application which requires timing requirements.     

人工智能应用中基于区间代数的时态推理

时态表示和推理是人工智能领域的重要研究内容之一,它的应用范围分布很广,从逻辑基础研究到知识系统的应用。区间代数是一种独立的与领域无关的时态理论。用区间代数能表示不确定的时态关系,可以很方便的用于时态推理,表达能力强;时态关系的区间表示比较直观,可理解性强;同时区间代数可以进一步扩展到二维空间领域,即将区间代数拓展为矩阵代数,实现二维空间推理。在一维时态推理中,将时态的区间表示和矩阵表示相结合,在提高计算效率的同时,保持了形象直观的时态表示。     

时间区间时序逻辑的判定性与表达能力

模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的,因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测,则并不清楚。约束时间域到非负实数,证明了其可满足性是不可判定的,但存在该逻辑的可判定子集,并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题,因此结果表明,时间区间时序逻辑不可模型检测,但其可判定子集可模型检测。     

时间自动机可达性分析中的状态空间约减技术综述

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可迭性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。     

Expressing and organizing real-time specification patterns via temporal logics

Formal specification models provide support for the formal verification and validation of the system behaviour. This advantage is typically paid in terms of effort and time spent in learning and using formal methods and tools. The introduction and usage of patterns have a double impact. They stand for examples on how to cover classical problems with formal methods in many different notations, so that the user can shorten the time to understand if a formal method can be used to meet his purpose and how it can be used. Furthermore, they are used for shortening the specification time, by reusing and composing different patterns to cover the specification, thus producing more understandable specifications which refer to commonly known patterns. For these reasons, both interests in and usage of patterns are growing and a higher number of proposals for patterns and pattern classification/organization has appeared in the literature. This paper reports a review of the state of the art for real-time specification patterns, so as to organize them in a unified way, while providing some new patterns which complete the unified model. The proposed organization is based on some relationships among patterns as demonstrated in the paper. During the presentation the patterns have been formalized in TILCO-X, whereas in appendix a list of patterns with formalizations in several different logics such as TILCO, LTL, CTL, GIL, QRE, MTL, TCTL and RTGIL, is provided disguised as links to the locations where such formalizations can be recovered and/or are directly reported, if found not accessible in the literature; this allows the reader to have a detailed view of all the classified patterns, including the ones already added. Furthermore, an example has been proposed to highlight the usefulness of the new identified patterns completing the unified model.     

Timed Behavior Trees for Failure Mode and Effects Analysis of time-critical systems

Behavior Trees are a graphical notation used for formalising functional requirements, and have been successfully applied to several industrial case studies. However, the standard notation does not support the concept of time, and consequently its application is limited to non-real-time systems. To overcome this limitation we extend the notation to timed Behavior Trees. We provide an operational semantics which is based on timed automata, and thus serves as a formal basis for the translation of timed Behavior Trees into the input notation of the timed model checker UPPAAL. System-level timing properties of a Behavior Tree model can then be automatically verified using UPPAAL. Based on the notational extensions with model checking support, we introduce timed Failure Mode and Effects Analysis, a process for identifying cause-consequence relationships between component failures and system hazards in real-time safety critical systems.     

Real-time refinement in Manna and Pnueli's temporal logic

A refinement calculus for the development of real-time systems is presented. The calculus is based upon a wide-spectrum language called TAM (the Temporal Agent Model), within which both functional and timing properties can be expressed in either abstract or concrete terms. A specification oriented semantics is given for the language. Program development is considered as a refinement process i.e. thecalculation of a structured program from an unstructured specification. An example program is developed.     

Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.     

Formalising a Value-Passing Calculus in HOL

Milner's value-passing calculus for describing and reasoning about communicating systems is formalised in the HOL proof assistant. Based on a previously defined mechanisation of pure CCS (no data communication, only synchronisation) in HOL, value-passing agents are given behavioural semantics by translating them into pure agents. An interactive proof environment is derived that supports both reasoning about the value-passing calculus and verification of value-passing specifications, which are defined over an infinite value domain. Received September 1997 / Accepted in revised form July 1999     

分布实时系统的概率规范和证明形式化

1引言 随着数字系统变得越来越小、越来越便宜,它们用于物理过程控制和与物理过程互协作的机会将越来越多。互相协作的过程如果出现意外行为,后果将可能很严重。这种意外为不仅仅指程序和数字     

启发式搜索在时间Petri网的共享资源调度中的应用

离散事件系统的调度规划问题是计算机科学的重要研究方向。本文介绍了如何在实际中将启发式算法同时提高搜索效率的方法。这在计算机和通信领域的资源调度问题方面有着较大的实用价值。     

Interval type-2 fuzzy expert system for prediction of carbon monoxide concentration in mega-cities

This paper presents an indirect approach to interval type-2 fuzzy logic system modeling to forecaste the level of air pollutants. The type-2 fuzzy logic system permits us to model the uncertainties among rules and the parameters related to data analysis. In this paper, we propose an indirect method to create an interval type-2 fuzzy logic system from a historical data, where Footprint of Uncertainties of fuzzy sets are extracted by implementation of an interval type-2 FCM algorithm and based on an upper and lower value for the level of fuzziness m in FCM. Finally, the proposed model is applied for prediction of carbon monoxide concentration in Tehran air pollution. It is shown that the proposed type-2 fuzzy logic system is superior in comparison to type-1 fuzzy logic systems in terms of two performance indices.     

在 XYZ/ E中实现混成实时系统——蒸气锅炉控制问题的解决

XYZ/E是一个时序逻辑系统,同时也是一种时序逻辑程序设计语言。XYZ/E能够在统一的框架下表示高层和低层的描述,所以便于软件系统的描述与实现。该文对基于XYZ/E的蒸气锅炉问题进行了描述与实现,并介绍了为该问题实现的图形用户界面.     

Towards a temporal coherence management in real-time knowledge-based systems

The multi-agent system paradigm emerges as an interesting approach in the Knowledge-Based System (KBS) field when distributed problem-solving techniques are required. On the other hand, temporal representation and reasoning problems arise in a wide range of KBS application areas where time plays a crucial role. In this paper, we show that when agents run concurrently and access common temporal data, some problems of coherence arise. We analyse the different cases in which an incoherence in temporal information can occur and provide a method to tackle this problem. In this method, conflict management is handled by means of exception handlers and control rules allowing the users to explicitly define their own strategy for temporal coherence solving.     

Deciding safety and liveness in TPTL

We show that deciding whether a TPTL formula describes a safety property is EXPSPACE-complete. Moreover, deciding whether a TPTL formula describes a liveness property is in 2-EXPSPACE. Our algorithms for deciding these problems extend those presented by Sistla [1] to decide the corresponding problems for LTL.