| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - Studujeme otázky verifikace třídy nekonečně stavových systémů známé jako wPAD. Tyto systémy slouží k modelování programů s (rekurzivním) voláním procedur a dynamickým vytvářením paralelních procesů. wPAD systémy odpovídají PAD systémům rozšířeným o acyklickou konečnou řídící jednotku. PAD systemy jsou pak kombinací prefixových přepisovacích systémů (zasobníkové systémy) a bezkontextových paralelních přepisovacích systémů (nesynchronizované Petriho sítě). Nedávno jsme představili symbolický algoritmus pro dosažitelnost v PAD systémech zalozený na stromových automatech s neomezeným větvením. V tomto článku zobecníme naše předchozí výsledky na třídu wPAD, která je striktně větší než PAD. Zmíněné zobecnění přináší kladnou odpověď na otevřenou otázku rozhodnutelnosti ověřování modelů pro wPAD a EF logiku. Také ukážeme, jak může být zmíněný symbolický algoritmus pro dosažitelnost použit k přibližné analýze synchronních PAD systémů. (cs)
- We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD.
- We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD. (en)
|
| Title
| - On Symbolic Verification of Weakly Extended PAD
- On Symbolic Verification of Weakly Extended PAD (en)
- Symbolicka verifikace slabe rozsirenych PAD (cs)
|
| skos:prefLabel
| - On Symbolic Verification of Weakly Extended PAD
- On Symbolic Verification of Weakly Extended PAD (en)
- Symbolicka verifikace slabe rozsirenych PAD (cs)
|
| skos:notation
| - RIV/00216224:14330/07:00021744!RIV08-MSM-14330___
|
| http://linked.open.../vavai/riv/strany
| |
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| - P(1M0545), Z(MSM0021622419)
|
| http://linked.open...iv/cisloPeriodika
| |
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/00216224:14330/07:00021744
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - rewrite systems; infinite-state systems; symbolic reachability analysis; model checking (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...odStatuVydavatele
| - DE - Spolková republika Německo
|
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...i/riv/nazevZdroje
| - Electronic Notes in Theoretical Computer Science
|
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...vavai/riv/projekt
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...v/svazekPeriodika
| |
| http://linked.open...iv/tvurceVysledku
| - Bouajjani, Ahmed
- Strejček, Jan
- Touili, Tayssir
|
| http://linked.open...n/vavai/riv/zamer
| |
| issn
| |
| number of pages
| |
| http://localhost/t...ganizacniJednotka
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)