Right-Universality of Visibly Pushdown Automata
In: ISSN: 0302-9743 ; Lecture Notes in Computer Science ; Runtime Verification ; 4th International Conference on Runtime Verification ; https://hal.archives-ouvertes.fr/hal-00946193 ; 4th International Conference on Runtime Verification, Sep 2013, Rennes, France. pp.76-93, ⟨10.1007/978-3-642-40787-1_5⟩, 2013
Online
Konferenz
Zugriff:
International audience ; Visibly pushdown automata (VPAs) express properties on structures with a nesting relation such as program traces with nested method calls. In the context of runtime verification, we are interested in the following problem: given u, the beginning of a program trace, and A, a VPA expressing a property to be checked on this trace, can we ensure that any extension uv of u will be accepted by A? We call this property right-universality w.r.t. u. We propose an online algorithm detecting at the earliest position of the trace, whether this trace is accepted by A. The decision problem associated with right-universality is ExpTime-complete. Our algorithm uses antichains and other optimizations, in order to avoid the exponential blow-up in most cases. This is confirmed by promising experiments conducted on a prototype implementation.
Titel: |
Right-Universality of Visibly Pushdown Automata
|
---|---|
Autor/in / Beteiligte Person: | Bruyère, Véronique ; Ducobu, Marc ; Gauwin, Olivier ; Université de Mons (UMons) ; Laboratoire Bordelais de Recherche en Informatique (LaBRI) ; Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB) ; Axel Legay, Saddek Bensalem ; CNRS PEPS, SOSP |
Link: | |
Zeitschrift: | ISSN: 0302-9743 ; Lecture Notes in Computer Science ; Runtime Verification ; 4th International Conference on Runtime Verification ; https://hal.archives-ouvertes.fr/hal-00946193 ; 4th International Conference on Runtime Verification, Sep 2013, Rennes, France. pp.76-93, ⟨10.1007/978-3-642-40787-1_5⟩, 2013 |
Veröffentlichung: | HAL CCSD ; Springer Berlin Heidelberg ; Springer, 2013 |
Medientyp: | Konferenz |
DOI: | 10.1007/978-3-642-40787-1_5 |
Schlagwort: |
|
Sonstiges: |
|