Bounded determinization of timed automata with silent transitions

Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major r...

Full description

Saved in:
Bibliographic Details
Published in:Real-time systems 2017-05, Vol.53 (3), p.291-326
Main Authors: Lorber, Florian, Rosenmann, Amnon, Ničković, Dejan, Aichernig, Bernhard K.
Format: Article
Language:English
Subjects:
Algorithms
Communications Engineering
Computer Science
Computer Systems Organization and Communication Networks
Control
Mechatronics
Model testing
Mutation
Networks
Observability (systems)
Performance and Reliability
Robotics
Special Purpose and Application-Based Systems
Test procedures
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Deterministic timed automata are strictly less expressive than their non-deterministic counterparts, which are again less expressive than those with silent transitions. As a consequence, timed automata are in general non-determinizable. This is unfortunate since deterministic automata play a major role in model-based testing, observability and implementability. However, by bounding the length of the traces in the automaton, effective determinization becomes possible. We propose a novel procedure for bounded determinization of timed automata. The procedure unfolds the automata to bounded trees, removes all silent transitions and determinizes via disjunction of guards. The proposed algorithms are optimized to the bounded setting and thus are more efficient and can handle a larger class of timed automata than the general algorithms. We show how to apply the approach in a fault-based test-case generation method, called model-based mutation testing, that was previously restricted to deterministic timed automata. The approach is implemented in a prototype tool and evaluated on several scientific examples and one industrial case study. To our best knowledge, this is the first implementation of this type of procedure for timed automata.
ISSN:0922-6443
1573-1383
DOI:10.1007/s11241-017-9271-x