Automated Predicate Abstraction for Real-Time Models

dc.contributor.authorBadban, Bahareh
dc.contributor.authorLeue, Stefan
dc.contributor.authorSmaus, Jan-Georgdeu
dc.date.accessioned2011-03-24T16:08:24Zdeu
dc.date.available2011-03-24T16:08:24Zdeu
dc.date.issued2009deu
dc.description.abstractWe present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata control locations and prunes the model, to compute a predicate abstraction of the model. We do so by taking information regarding control locations and their newly computed invariants into account. We also discuss a prototype implementation of our technique.eng
dc.description.versionpublished
dc.format.mimetypeapplication/pdfdeu
dc.identifier.ppn318103168deu
dc.identifier.urihttp://kops.uni-konstanz.de/handle/123456789/5960
dc.language.isoengdeu
dc.legacy.dateIssued2010deu
dc.rightsterms-of-usedeu
dc.rights.urihttps://rightsstatements.org/page/InC/1.0/deu
dc.subject.ddc004deu
dc.titleAutomated Predicate Abstraction for Real-Time Modelseng
dc.typeINPROCEEDINGSdeu
dspace.entity.typePublication
kops.citation.bibtex
@inproceedings{Badban2009Autom-5960,
  year={2009},
  title={Automated Predicate Abstraction for Real-Time Models},
  author={Badban, Bahareh and Leue, Stefan and Smaus, Jan-Georg},
  note={Accepted for publication in: International Workshop on Verification of Infinite-State Systems (INFINITY 2009) EPTCS 10, 2009, pp. 36-43}
}
kops.citation.iso690BADBAN, Bahareh, Stefan LEUE, Jan-Georg SMAUS, 2009. Automated Predicate Abstraction for Real-Time Modelsdeu
kops.citation.iso690BADBAN, Bahareh, Stefan LEUE, Jan-Georg SMAUS, 2009. Automated Predicate Abstraction for Real-Time Modelseng
kops.citation.rdf
<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/server/rdf/resource/123456789/5960">
    <dcterms:title>Automated Predicate Abstraction for Real-Time Models</dcterms:title>
    <dc:creator>Smaus, Jan-Georg</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:rights>terms-of-use</dc:rights>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5960/1/Automated_Predicate_Abstraction_for_Real_Time_Models_2009_KOPS10599.pdf"/>
    <dcterms:issued>2009</dcterms:issued>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:language>eng</dc:language>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5960/1/Automated_Predicate_Abstraction_for_Real_Time_Models_2009_KOPS10599.pdf"/>
    <dc:format>application/pdf</dc:format>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:creator>Leue, Stefan</dc:creator>
    <dc:contributor>Badban, Bahareh</dc:contributor>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5960"/>
    <dc:creator>Badban, Bahareh</dc:creator>
    <dcterms:abstract xml:lang="eng">We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata control locations and prunes the model, to compute a predicate abstraction of the model. We do so by taking information regarding control locations and their newly computed invariants into account. We also discuss a prototype implementation of our technique.</dcterms:abstract>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:08:24Z</dcterms:available>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:08:24Z</dc:date>
    <dc:contributor>Smaus, Jan-Georg</dc:contributor>
  </rdf:Description>
</rdf:RDF>
kops.description.commentAccepted for publication in: International Workshop on Verification of Infinite-State Systems (INFINITY 2009) EPTCS 10, 2009, pp. 36-43deu
kops.description.openAccessopenaccessgreen
kops.flag.knbibliographytrue
kops.identifier.nbnurn:nbn:de:bsz:352-opus-105997deu
kops.opus.id10599deu
relation.isAuthorOfPublication7836390d-fc5b-4523-a272-2f8f5025bf3f
relation.isAuthorOfPublicationa0cf1380-ebf9-403b-a02e-6e97bae25ef6
relation.isAuthorOfPublication.latestForDiscovery7836390d-fc5b-4523-a272-2f8f5025bf3f

Dateien

Originalbündel

Gerade angezeigt 1 - 1 von 1
Vorschaubild nicht verfügbar
Name:
Automated_Predicate_Abstraction_for_Real_Time_Models_2009_KOPS10599.pdf
Größe:
97.04 KB
Format:
Adobe Portable Document Format