Reachability results for timed automata with unbounded data structures

Systems of Data Management Timed Automata (SDMTAs) are networks of communicating timed automata with structures to store messages and functions to manipulate them. We prove the decidability of the reachability problem for a subclass of SDMTAs which assumes an unbounded knowledge, and we analyze the expressiveness of the model and the considered subclass. In particular, while SDMTAs can simulate a Turing machine, and hence the reachability problem is in general undecidable, the subclass for which reachability is decidable, when endowed with a concept of recognized language, accepts languages that are not regular. As an application, we model and analyze a variation of the Yahalom protocol.     

Efficient verification of timed automata with BDD-like data structures

We investigate the effect on efficiency of various design issues for BDD-like data structures of TA state space representation and manipulation. We find that the efficiency is highly sensitive to decision atom design and canonical form definition. We explore the two issues in detail and propose to use CRD (Clock-Restriction Diagram) for TA state space representation and present algorithms for manipulating CRD in the verification of TAs. We compare three canonical forms for zones, develop a procedure for quick zone-containment detection, and present algorithms for verification with backward reachability analysis. Three possible evaluation orderings are also considered and discussed. We implement our idea in our tool Red 4.2 and carry out experiments to compare with other tools and various strategies of Red in both forward and backward analysis. Finally, we discuss the possibility of future improvement.     

Implicit integration of scenarios into a reduced timed automaton

We aim at synthesizing an executable specification for a real-time reactive system by integrating real-time scenarios into a reduced timed automaton (TA). A scenario is a part of the specification of a system behavior. The integration of scenarios into a single TA is based on its formal semantics. The TA, which results from the integration of a set of scenarios, is independent of the order in which the scenarios are added to. We also present an algorithm to reduce such resulting TA in order to prevent combinatorial explosion.     

Mapping timed cause-effect structures into timed petri nets

Conclusion The problem of inverse mapping of Petri nets into CES remains an interesting open question. Raczunas [5] claims that it is not for every PN that a strictly equivalent CES exists. He accordingly proposes weak equivalence of this mapping. Kotov [6] defines a topologically structured subclass of PN—regular PN. The subclass of regular PN has the same cardinality as the class of all PN in the sense of behavioral equivalence. It is therefore relevant to compare the class of regular PN with CES. The study was partially financed by the Russian Foundation for Basic Research, grant No. 93-012-986. Translated from Kibernetika i Sistemnyi Analiz, No. 2, pp. 44–54, March–April, 1997.     

Physical hypermedia: Augmenting physical material with hypermedia structures

This paper introduces the notion of physical hypermedia, addressing the problem of organizing material in mixed digital and physical environments. Based on empirical studies, we propose concepts for collectional actions and meta-data actions, and present prototypes combining principles from augmented reality and hypermedia to support organization of mixtures of digital and physical materials. Our prototype of a physical hypermedia system is running on an augmented architect's desk and digital walls utilizing Radio Frequency Identifier (RFID) tags as well as visual tags tracked by cameras. It allows users to tag physical materials, and have these tracked by readers (antennas) that may become pervasive in our work environments. In the physical hypermedia system, we work with three categories of RFID tags: simple object tags, collectional tags, and tooltags invoking operations such as grouping and linking of physical material. In addition, we utilize visual ARToolKit tags for linking and navigating 3D models on a physical desk. Our primary application domain is architecture and design, and so we discuss the use of augmented collectional artifacts primarily for this domain.     

Distributed inversion in timed discrete event systems

We consider a discrete event system (DES) modeled by a timed automaton with partial state and event observations. We view the system as an input-output system, where the input is a sequence of event lifetimes, and the output is the resulting sequence of events, states, and transition epochs. We consider the problem of extracting event lifetimes (input) from observations of the output trajectory, which we callinversion. We give necessary and sufficient conditions forinvertibility, and an algorithm that extracts event lifetimes from any given output observation of an invertible system. We describe a distributed timed DES model based on the prioritized synchronous product of subsystems, and study the inversion problem in this framework. We show that invertibility in the subsystems implies invertibility in the global system. To illustrate our results, we provide an example of a tandem network.     

Verification in loosely synchronous queue-connected discrete timed automata

We look at a model of a queue system that consists of the following components:

1. Two discrete timed automata W (the “writer”) and R (“the reader”).

2. One unrestricted queue that can be used to send messages from W to R. There is no bound on the length of the queue.

W and R do not share a global clock and operate in a loosely synchronous way. That is, the absolute value of the difference between the local time of W and the local time of R is always bounded by a positive constant. We show that the binary reachability for these systems is effectively computable, and this result is generalized to the case when there are two queues (one from W to R and the other from R to W) that operate in half-duplex. We then present some properties (e.g., safety, invariance, etc.) that can be verified for loosely synchronous queue-connected discrete timed automata and give an example of a system composed of a sensor and a controller that is verifiable using our results.     

Semantic domains of timed event structures

In the paper, timed extensions of various classes of event structures and marked Scott domains are studied, categories of these models are constructed, and their properties are examined. In addition, based on category-theoretic methods, relationship between the timed structures and marked Scott domains is established.     

Template languages for fault monitoring of timed discrete eventprocesses

This paper introduces a new framework for modeling discrete event processes. This framework, called condition templates, allows the modeling of processes in which both single-instance and multiple-instance behaviors are exhibited concurrently. A single-instance behavior corresponds to a trace from a single finite-state process, and a multiple-instance behavior corresponds to the timed interleavings of an unspecified number of identical processes operating at the same time. The template framework allows the modeling of correct operation for systems consisting of concurrent mixtures of both single and multiple-instance behaviors. This representation can then be used in online fault monitoring for confirming the correct operation of a system. We compare the class of timed languages representable by template models with classes of timed languages from timed automata models. It is shown that templates are able to model timed languages corresponding to single and multiple-instance behaviors and combinations thereof. Templates can thus represent languages that could not be represented or monitored using timed automata alone     

Augmenting training data with syntactic phrasal-segments in low-resource neural machine translation

Machine Translation - Neural machine translation (NMT) has emerged as a preferred alternative to the previous mainstream statistical machine translation (SMT) approaches largely due to its ability...     

Fault diagnosis of timed discrete event systems using Dioid Algebra

This paper deals with the fault diagnosis problem in a concurrent Timed Discrete Event System (TDES). In a TDES, concurrency leads to more complexity in the diagnoser and appears where, at a certain time, some user must choose among several resources. To cope with this problem, a new model-based diagnoser is proposed in this paper. This diagnoser uses Durational Graph (DG), a main subclass of timed automata for representing the time evolution of the TDES. The proposed diagnoser predicts all possible timed-event trajectories that may be generated by the DG. This prediction procedure is complicated for nondeterministic DG’s that are obtained for concurrent TDES’s. To solve this problem, a new Dioid Algebra, Union-Plus Algebra is introduced in this paper. Based on this Algebra, a reachability matrix is defined for a DG that plays an essential role in predicting the time behavior of TDES. By using reachability matrix, a prediction procedure is carried on via an effective equation set that is similar to linear system state equations in ordinary algebra. These results provide a suitable framework for designing an observer-based diagnoser that is illustrated by an example.     

Control synthesis of timed discrete event systems based onpredicate invariance

In this paper, arc-timed Petri nets are used to model controlled real-time discrete event systems, and the control synthesis problem that designs a controller for a system to satisfy its given closed-loop behavior specification is addressed. For the problem with the closed-loop behavior specified by a state predicate, real-time control-invariant predicates are introduced, and a fixpoint algorithm to compute the unique extremal control-invariant subpredicate of a given predicate, key to the control synthesis, is presented. For the problem with the behavior specified by a labeled arc-timed Petri net, it is shown that the control synthesis problem can be transformed into one that synthesizes a controller for an induced arc-timed Petri net with a state predicate specification. The problem can then be solved by using the fixpoint algorithm as well. The algorithm involves conjunction and disjunction operations of polyhedral sets and can be algorithmically implemented, making automatic synthesis of controllers for real-time discrete event systems possible.     

随机计时离散事件系统的软控制任务研究

本文通过引入马氏决策过程中的迭代算法,研究了计时离散事件系统的随机优化监控综合问题。为了对不确定的人造系统实施监控,在考虑事件的操作时间的基础上,利用带有发生事件概率分布函数的随机计时离散事件系统模型对系统建模。为了对这类随机系统实施监控,在传统方法中,采用控制任务的最大可控子语言设计控制器,不能体现系统模型的随机特性。本文提出利用软控制任务代替原控制任务的方法,使其超出原控制任务的概率在给定的容许度约束范围内。首先,通过在计时离散事件系统中定义计时事件的发生概率映射和发生费用函数,利用离散事件系统的逻辑特性,构造事件发生序列的期望费用函数,进而确立马氏决策过程的最优方程,建立软控制任务与期望费用函数之间的关系。然后,通过计算事件发生序列的费用值,提出利用有限费用值可以用来确定软控制任务,进而基于逻辑监控方法,确定最优监控器。最后,利用计算有限费用值的迭代过程,提出迭代算法,并给出了计算实例。     

Experimenting with data structures

Research in robust data structures can be done both by theoretical analysis of properties of abstract implementations and by empirical study of real implementations. Empirical study requires a support environment for the actual implementation. In particular, if the response of the implementation to errors is being studied, a mechanism must exist for artificially injecting appropriate kinds of errors. This paper discusses techniques used in empirical investigations of data structure robustness, with particular reference to tools developed for this purpose at the University of Waterloo.     

Augmenting photographs with audio

We report a user requirements study of several interfaces for the playback of sounds from photographs. The study showed that users liked listening to audiophotos when the sounds are played back from photographic prints, but as a complement to playback on a PC. When handling prints the audio needs to be invoked manually from the print with a facility to pause the audio during playback. A handheld audioprint player was then designed to fulfill these needs, based on an embedded chip in the paper.     

Suboptimal control of bunches of trajectories of discrete deterministic automaton time-invariant systems

The optimal control problem for discrete deterministic time-invariant automaton systems under parametric uncertainty is considered. The changes in the state (switching) of the system are described by a recurrence equation. The switching times and their number are not specified in advance—they are found by optimization. The initial state of the system is not known exactly. For this reason, the problems of finding the optimal on the average and the optimal guaranteeing (minimax) controls of bunches of trajectories are formulated. It is proposed to solve these problems using the separation principle, which assumes that the bunch is controlled using the control that is optimal for a specially chosen individual trajectory in the bunch. Generally, this control is suboptimal. Algorithms for the synthesis of suboptimal control of bunches are developed. It is proved that, in the linear-quadratic time-invariant problems, the suboptimal bunch control is optimal on the average or is the optimal minimax control, depending on the problem being solved.     

State based control of timed discrete event systems using binary decision diagrams

This work discusses a new synthesis approach to the supervisory control of timed discrete event systems (TDES), that is more efficient than the existing approaches. With this method, many practical systems can be synthesized on a personal computer. The method exploits binary decision diagrams (BDDs), adapted to the specific structure of TDES. It is shown that the number of nodes in the BDD representing a TDES can be a better measure of the complexity of the TDES than the number of states and transitions. Structural information based on the ‘timers’ for a given TDES together with the reduction properties of BDDs contributes to efficient performance. The success of our approach is illustrated with large versions of an existing example taken from the literature.     

An algebraic approach to data languages and timed languages

Algebra offers an elegant and powerful approach to understand regular languages and finite automata. Such framework has been notoriously lacking for timed languages and timed automata. We introduce the notion of monoid recognizability for data languages, which includes timed languages as special case, in a way that respects the spirit of the classical situation. We study closure properties and hierarchies in this model and prove that emptiness is decidable under natural hypotheses. Our class of recognizable languages properly includes many families of deterministic timed languages that have been proposed until now, and the same holds for non-deterministic versions.