Wyniki wyszukiwania - BazTech

1

Distributed Timed Automata with Independently Evolving Clocks

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

Fundamenta Informaticae

|

2014

|

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.

2

Uniform Satisfiability in PSPACE for Local Temporal Logics Over Mazurkiewicz Traces

Gastin P., Kuske D.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

169-197

EN

We study the complexity of temporal logics over concurrent systems that can be described by Mazurkiewicz traces. We develop a general method to prove that the uniform satisfiability problem of local temporal logics is in PSPACE. We also demonstrate that this method applies to all known local temporal logics.

3

Characterization of the expressive power of silent transitions in timed automata

Berard B., Petit A., Diekert V., Gastin P.

Fundamenta Informaticae

|

1998

|

Vol. 36, nr 2,3

145-182

EN

Timed automata are among the most widely studied models for real-time systems. Silent transitions, i.e., e-transitions, have already been proposed in the original paper on timed automata by Alur and Dill. We show that class TLe of timed languages recognized by automata with e-transitions, is more robust and more expressive than the corresponding class TL without e-transitions. We then focus on e-transitions without reset, i.e. e-transitions which do not reset clocks. We propose an algorithm to construct, given a timed automaton, an equivalent one without such transitions. This algorithm is in two steps, it first suppresses the cycles of e-transitions without reset and then the remaining ones. Then, we prove that a timed automaton such that no e-transition which resets clocks lies on any directed cycle, can be effectively transformed into a timed automaton without e-transitions. Interestingly, this main result holds under the assumption of non-Zenoness and it is false otherwise. To complete the picture, we exhibit a simple timed automaton with an e-transition, which resets some clock, on a cycle and which is not equivalent to any e-free timed automaton. To show this, we develop a promising new technique based on the notion of precise action.