Wyniki wyszukiwania - Biblioteka Nauki

1

Universality Analysis for One-Clock Timed Automata

100%

Abdulla P. A. , Deneux J. , Ouaknine J. , Quaas K. , Worrell J.

|

2008

|

tom Vol. 89, nr 4

419-450

EN

This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if ε-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.

2

Distributed Timed Automata with Independently Evolving Clocks

63%

Akshay S. , Bollig B. , Gastin P. , Mukund M. , Kumar K. N.

Fundamenta Informaticae

|

2014

|

tom Vol. 130, nr 4

377--407

EN

We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.

3

SAT-based Unbounded Model Checking of Timed Automata

63%

Penczek W. , Szreter M.

|

2008

|

tom Vol. 85, nr 1-4

425-440

EN

We present an improvement to the SAT-based Unbounded Model Checking (UMC, for short) algorithm [13]. Our idea consists in building blocking clauses of literals corresponding not only to propositional variables encoding states, but also to more general subformulas over these variables encoding sets of states. This way our approach alleviates an exponential blow-up in the number of blocking clauses. A hybrid algorithm for verifying Timed Automata is proposed, where the timed part of blocking clauses is computed using Difference Bound Matrices. The optimization results in a considerable reduction in the size and the number of generated blocking clauses, thus improving the overall performance. This is shown on the standard benchmark of Fischer's Mutual Exclusion protocol.

4

Runtime Monitoring of Contract Regulated Web Services

63%

Lomuscio A. , Penczek W. , Solanki M. , Szreter M.

|

2011

|

tom Vol. 111, nr 3

339-353

EN

We investigate the problem of locally monitoring contract regulated behaviours in agentbased web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.

5

SAT-Based Reachability Checking for Timed Automata with Discrete Data

63%

Zbrzezny A. , Półrola A.

|

2007

|

tom Vol. 79, nr 3-4

579-593

6

Path Compression in Timed Automata

63%

Janowska A. , Penczek W.

|

2007

|

tom Vol. 79, nr 3-4

379-399

EN

The paper presents a method of abstraction for timed systems. To extract an abstract model of a timed system we propose to use static analysis, namely a technique called path compression. The idea behind the path compression consists in identifying a path (or a set of paths) on which a process executes a sequence of transitions that do not influence a property being verified, and replacing this path with a single transition. The method is property driven since it depends on a formula in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL*-X.

7

Checking Reachability Properties for Timed Automata via SAT

63%

Woźna B. , Zbrzezny A. , Penczek W.

|

2003

|

tom Vol. 55, nr 2

223-241

EN

The paper deals with the problem of checking reachability for timed automata. The main idea consists in combining the well-know forward reachability algorithm and the Bounded Model Checking (BMC) method. In order to check reachability of a state satisfying some desired property, first the transition relation of a timed automaton is unfolded iteratively to some depth and encoded as a propositional formula. Next, the desired property is translated to a propositional formula and the satisfiability of the conjunction of the two defined above formulas is checked. The unfolding of the transition relation can be terminated when either a state satisfying the property has been found or all the states of the timed automaton have been searched. The efficiency of the method is strongly supported by the experimental results.

8

Verification of Timed Automata Based on Similarity

63%

Dembiński P. , Penczek W. , Półrola A.

|

tom Vol. 51, nr 1,2

59-89

EN

The paper presents a modification of the standard partitioning technique to generate abstract state spaces preserving similarity for Timed Automata. Since this relation is weaker than bisimilarity, most of the obtained models (state spaces) are smaller than bisimilar ones, but still preserve the universal fragments of branching time temporal logics. The theoretical results are exemplified for strong, delay, and observational simulation relations.

9

A Notion of Non-Interference for Timed Automata

63%

Barbuti R. , De Francesco N. , Santone A. , Tesei L.

|

tom Vol. 51, nr 1,2

1-11

EN

The non-interference property of concurrent systems is a security property concerning the flow of information among different levels of security of the system. In this paper we introduce a notion of timed non-interference for real-time systems specified by timed automata. The notion is presented using an automata based approach and then it is characterized also by operations and equivalence between timed languages. The definition is applied to an example of a time-critical system modeling a simplified control of an airplane.

10

A Decidable Notion of Timed Non-Interference

63%

Barbuti R. , Tesei L.

|

2003

|

tom Vol. 54, nr 2,3

137-150

EN

We present a notion of non-interference which embodies the notion of time. It is useful to verify the strength of a system against attacks depending on the frequency of certain actions. In particular we give a decidable definition of non-interference which can be checked by using existing verification tools. We show an application example of our notion of non-interference by defining a variant of the classical Fischer's mutual exclusion protocol and by analyzing its strength against attacks.

11

Blending Timed Formal Models with Clock Transition Systems

51%

Jard C. , Lime D. , Roux O. H.

Fundamenta Informaticae

|

2014

|

tom Vol. 129, nr 1/2

85--100

EN

Networks of Timed Automata (NTA) and Time Petri Nets (TPNs) are well-established formalisms used to model, analyze and control industrial real-time systems. The underlying theories are usually developed in different scientific communities and both formalisms have distinct strong points: for instance, conciseness for TPNs and a more flexible notion of urgency for NTA. The objective of the paper is to introduce a new model allowing the joint use of both TPNs and NTA for the modeling of timed systems. We call it Clock Transition System (CTS). This new model incorporates the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency is introduced by a separate description of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational semantics and provide (syntactic) translations. The classical state-space computation developed for NTA and then adapted to TPNs can easily be defined for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and practical model to factor out the upcoming developments in the TPNs and the NTA scientific communities.

12

Classes of Timed Automata and the Undecidability of Universality

51%

Moura A. V. , Pinto G. A.

|

2008

|

tom Vol. 82, nr 1-2

171-184

EN

Universality for deterministic Timed Büchi Automata (TBA) is PSPACE-complete but becomes highly undecidable when unrestricted nondeterminism is allowed. More precisely, universality for nondeterministic TBA is P11-hard and its precise position in the analytical hierarchy is still an open question. In this paper we introduce two types of syntactical restrictions to nondeterministic TBA, which are of independent interest, and show that their universality problem is P11-complete. These restrictions define, as we prove, proper subclasses of the class of timed languages defined by nondeterministic TBA. This suggests, as we argue, that no solution to that open question will come without surprise. We also establish closure properties and the relationships between the classes of languages we describe.

13

Timed Cooperating Automata

51%

Lanotte R. , Maggiolo-Schettini A.

|

2000

|

tom Vol. 43, Nr 1-4

153-173

EN

We propose Timed Cooperating Automata (TC As), an extension of the model Cooperating Automata of Harel and Drusinsky, and we investigate some basic properties. In particular we consider variants of TCAs based on the presence or absence of internal activity, urgency and reactivity, and we compare the expressiveness of these variants with that of the classical model of Timed Automata (TAs) and its extensions with periodic clock constraints and with silent moves. We consider also closure and decidability properties of TCAs and start a study on succinctness of their variants with respect to that of TAs.

14

Towards Verification of Java Programs in VerICS

51%

Zbrzezny A. , Woźna B.

|

2008

|

tom Vol. 85, nr 1-4

533-548

EN

VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java. # Greedy Algorithm for Attribute Reduction

15

Translation of Intermediate Language to Timed Automata with Discrete Data

51%

Janowska A. , Janowski P. , Wróblewski D.

|

2008

|

tom Vol. 85, nr 1-4

235-248

EN

The aim of this work is to describe the translation from Intermediate Language, one of the input formalisms of the model checking platform VerICS, to timed automata with discrete data and to compare it with the translation to classical timed automata. The paper presents syntax and semantics of both formalisms, the translation rules as well as a simple example.

16

Timed Automata with non-Instantaneous Actions

51%

Barbuti R. , De Francesco N. , Tesei L.

|

2001

|

tom Vol. 47, nr 3,4

189-200

EN

In this paper we propose a model, timed automata with non-instantaneous actions, which allows representing in a suitable way real-time systems. Timed automata with non-instantaneous actions extend the timed automata model by dropping the assumption that actions are instantaneous: in our model an action can take some time to be completed. We investigate the expressiveness of the new model, comparing it with classical timed automata. In particular, we study the set of timed languages which can be accepted by timed automata with non-instantaneous actions. We prove that timed automata with non-instantaneous actions are more expressive than timed automata and less expressive than timed automata with e edges. Moreover we define the parallel composition of timed automata with non-instantaneous actions. We point out how the specification by means of a parallel timed automaton with non-instantaneous actions is, in some cases, more convenient to represent reality.

17

Transformations of Timed Cooperating Automata

51%

Lanotte R. , Maggiolo-Schettini A. , Tini S. , Peron A.

|

2001

|

tom Vol. 47, nr 3,4

271-282

EN

The paper pursues the investigation of Timed Cooperating Automata (TCAs) by studying transformations which are suggested as means for stepwise TCA construction.

18

Undecidability Results for Timed Automata with Silent Transitions

51%

Bouyer P. , Haddad S. , Reynier P.-A.

|

2009

|

tom Vol. 92, nr 1-2

1-25

EN

In this work, we study decision problems related to timed automata with silent transitions (TAε) which strictly extend the expressiveness of timed automata (TA). We first answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TAε can be recognized by some TA? Then we establish in the framework of TAε some old open conjectures that O. Finkel has recently solved for TA. His proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TAε , the proofs in the framework of TAε thus require more elaborated arguments. We establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We also show these results in the framework of infinite timed languages.

19

Recognition of actions in meeting videos using timed automata

51%

Pelc L. , Kwolek B.

Machine Graphics and Vision

|

2006

|

tom Vol. 15, No. 3/4

577-584

EN

This paper addresses the problem of action recognition in meeting videos. A declarative knowledge provided graphically by the user together with person positions extracted by a tracking algorithm are used to generate the data for recognition. The actions have been formally specified using timed automata. The specification was verified on the basis of simulation tests as well as an analysis. The tracking is accomplished using a particle filter built on cues such as color, gradient and shape.

20

Verification of FlexRay start-up mechanism by timed automata

51%

Malinský J. , Novák J.

Metrology and Measurement Systems

|

2010

|

tom Vol. 17, nr 3

461-480

EN

This contribution deals with the modelling of a selected part of a new automotive communication standard called FlexRay. In particular, it focuses on the mechanism ensuring the start-up of a FlexRay network. The model has been created with the use of timed automata and verified. For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of suitable queries compiled in the so called computation tree logic. This model can be used to look for incorrect settings of time parameters of communication nodes in the network that prevent network start-up and subsequently the start of the car. The existence of this model also opens the way for finding possible errors in the standard. On the basis of the model, the work gives a case study of the start-up mechanism behaviour verification in a FlexRay network consisting of three communication nodes.