Academic
Publications
Removing epsilon-Transitions in Timed Automata

Removing epsilon-Transitions in Timed Automata,10.1007/BFb0023491,Volker Diekert,Paul Gastin,Antoine Petit

Removing epsilon-Transitions in Timed Automata   (Citations: 13)
BibTex | RIS | RefWorks Download
. Timed automata are among the most widely studied modelsfor real-time systems. Silent transitions, i.e., "-transitions, have alreadybeen proposed in the original paper on timed automata by Alur and Dill[2]. In [7] it is shown that "-transitions can be removed, if they do notreset clocks; moreover "-transitions strictly increase the power of timedautomata, if there is a self-loop containing "-transitions which reset someclocks. The authors of [7] left open the problem about the power of...
Cumulative Annual
    • ...It is also not in general possible to remove internal transitions from a timed automata (and when they can, it may be very costly) [61]...

    Anders Hesselet al. Testing Real-Time Systems Using UPPAAL

    • ...Several authors brought solutions that consist in determinizing explicitly the specification (see, e.g., [17], [27]); although [1] demonstrated that (1) TA cannot be determinized in general, and (2) that it is sometimes impossible to withdraw internal actions [20]...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...Observe that any trace of the implementation I1([40, 40],[20, 20]) (in any environment) can be matched by the specification; hence I1([40, 40],[20,20]) rswtiocoEU QC. Thus also I1([40,40],[20,20]) rswtiocoE1 QC. In contrast, I1([70,70],[5,5]) rswtiocoEU QC for tow reasons: 1) it has the timed trace: coin.30.req.5...
    • ...We have I2([40,40],[20,20]) rswtiocoEU QC and I2([40,40],[20,20]) rswtiocoE1 QC because it has the timed trace: coin.30.req.10 (tackeCup,lightCoffee).2.(returnCup,lightCoffee).5 .lightCoffee that QC does not...
    • ...We have I2([40,40],[20,20]) rswtiocoEU QC and I2([40,40],[20,20]) rswtiocoE1 QC because it has the timed trace: coin.30.req.10 (tackeCup,lightCoffee).2.(returnCup,lightCoffee).5 .lightCoffee that QC does not...
    • ...We have I2([40,40],[20,20]) rswtiocoEU QC and I2([40,40],[20,20]) rswtiocoE1 QC because it has the timed trace: coin.30.req.10 (tackeCup,lightCoffee).2.(returnCup,lightCoffee).5 .lightCoffee that QC does not...
    • ...We have I2([40,40],[20,20]) rswtiocoEU QC and I2([40,40],[20,20]) rswtiocoE1 QC because it has the timed trace: coin.30.req.10 (tackeCup,lightCoffee).2.(returnCup,lightCoffee).5 .lightCoffee that QC does not...
    • ...In contrast, I2([40, 40],[20, 20]) rswtiocoEC QC and I2([40, 40],[20, = 60 20]) rswtiocoE1 QC if [ [ ∞ Rd because EC never takes up his cup while the machine preparing coffee and E1 (60) never requests light coffee...
    • ...In contrast, I2([40, 40],[20, 20]) rswtiocoEC QC and I2([40, 40],[20, = 60 20]) rswtiocoE1 QC if [ [ ∞ Rd because EC never takes up his cup while the machine preparing coffee and E1 (60) never requests light coffee...

    Noureddine Adjiret al. Test of preemptive real-time systems

    • ...However, for expressive formalisms like timed automata this approach is infeasible because in general they cannot be determinized [2] and their unobservable actions cannot always (and when they can it may be very costly) be removed [29]...

    Kim Guldstrand Larsenet al. Online Testing of Real-time Systems Using Uppaal

    • ...However, for expressive formalisms like timed automata this approach is infeasible because in general they cannot be determinized [2] and their unobservable actions cannot always (and when they can it may be very costly) be removed [34]...

    Kim Guldstrand Larsenet al. Online Testing of Real-Time Systems Using UPPAAL: Status and Future Wo...

    • ...In addition, internal actions increase the expressiveness of timed automata, and specifically it has been shown that internal actions with clock resets on cycles cannot be removed [40]...

    Brian Nielsenet al. Automated Test Generation from Timed Automata

Sort by: