School of Computing

On time and action lock free description of timed systems

H. Bowman

Technical Report 16-99, Computing Laboratory, University of Kent at Canterbury, December 1999.

Abstract

Time and action locks can arise freely in timed automata specification. While both are error situations, time locks are by far the more serious fault. This is because their occurrence prevents any further evolution of the system. First we investigate techniques for avoiding the occurrence of timelocks. The central aspect of our solution is a redefinition of automata parallel composition based on the Timed Automata with Deadlines Framework of Bornot and Sifakis. Then the second result we present is a notion of parallel composition which preserves action lock freeness. In the sense that, if any component automaton is action lock free, then the composition will also be action lock free.

Download publication 898 kbytes (PostScript)

Bibtex Record

@techreport{1188,
author = {H. Bowman},
title = {On Time and Action Lock Free Description of Timed Systems},
month = {December},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/1188},
    publication_type = {techreport},
    submission_id = {1804_986210996},
    institution = {Computing Laboratory, University of Kent at Canterbury},
    type = {Technical Report},
    number = {16-99},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014