KOPS - The Institutional Repository of the University of Konstanz

A livelock freedom analysis for infinite state asynchronous reactive systems

A livelock freedom analysis for infinite state asynchronous reactive systems

Cite This

Files in this item

Checksum: MD5:eb89a14bf0b44edf7a80ac002a6b018e

LEUE, Stefan, Alin ŞTEFĂNESCU, Wei WEI, 2006. A livelock freedom analysis for infinite state asynchronous reactive systems. In: BAIER, Christel, ed., Holger HERMANNS, ed.. CONCUR 2006 – Concurrency Theory. Berlin, Heidelberg:Springer Berlin Heidelberg, pp. 79-94. ISBN 978-3-540-37376-6. Available under: doi: 10.1007/11817949_6

@inproceedings{Leue2006livel-21550, title={A livelock freedom analysis for infinite state asynchronous reactive systems}, year={2006}, doi={10.1007/11817949_6}, number={4137}, isbn={978-3-540-37376-6}, address={Berlin, Heidelberg}, publisher={Springer Berlin Heidelberg}, series={Lecture Notes in Computer Science}, booktitle={CONCUR 2006 – Concurrency Theory}, pages={79--94}, editor={Baier, Christel and Hermanns, Holger}, author={Leue, Stefan and Ştefănescu, Alin and Wei, Wei} }

<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/21550"> <dc:contributor>Ştefănescu, Alin</dc:contributor> <dcterms:rights rdf:resource="https://kops.uni-konstanz.de/page/termsofuse"/> <dc:rights>terms-of-use</dc:rights> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21550"/> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21550/2/leue_215507.pdf"/> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:bibliographicCitation>CONCUR 2006 - concurrency theory : 17th International Conference, CONCUR 2006, Bonn, Germany, August 27 - 30, 2006; proceedings / Christel Baier ... (Eds.).- Berlin [u.a.] : Springer, 2006. - S. 79-94. - (Lecture notes in computer science ; 4137). - ISBN 978-3-540-37376-6</dcterms:bibliographicCitation> <dc:creator>Leue, Stefan</dc:creator> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21550/2/leue_215507.pdf"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-04T08:51:13Z</dc:date> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-04T08:51:13Z</dcterms:available> <dcterms:abstract xml:lang="eng">We describe an incomplete but sound and efficient livelock freedom test for infinite state asynchronous reactive systems. The method abstracts a system into a set of simple control flow cycles labeled with their message passing effects. From these cycles, it constructs a homogeneous integer programming problem (IP) encoding a necessary condition for the existence of livelock runs. Livelock freedom is assured by the infeasibility of the generated homogeneous IP, which can be checked in polynomial time. In the case that livelock freedom cannot be proved, the method proposes a counterexample given as a set of cycles. We apply an automated cycle dependency analysis to counterexamples to check their spuriousness and to refine the abstraction. We illustrate the application of the method to Promela models using our prototype implementation named aLive.</dcterms:abstract> <dc:contributor>Wei, Wei</dc:contributor> <dc:language>eng</dc:language> <dc:creator>Ştefănescu, Alin</dc:creator> <dcterms:issued>2006</dcterms:issued> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:creator>Wei, Wei</dc:creator> <dcterms:title>A livelock freedom analysis for infinite state asynchronous reactive systems</dcterms:title> </rdf:Description> </rdf:RDF>

Downloads since Oct 1, 2014 (Information about access statistics)

leue_215507.pdf 92

This item appears in the following Collection(s)

Search KOPS


Browse

My Account