Verification of Flat FIFO Systems
The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establish...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5999/pdf |
| _version_ | 1797268548960124928 |
|---|---|
| author | Alain Finkel M. Praveen |
| author_facet | Alain Finkel M. Praveen |
| author_sort | Alain Finkel |
| collection | DOAJ |
| description | The decidability and complexity of reachability problems and model-checking
for flat counter machines have been explored in detail. However, only few
results are known for flat (lossy) FIFO machines, only in some particular cases
(a single loop or a single bounded expression). We prove, by establishing
reductions between properties, and by reducing SAT to a subset of these
properties that many verification problems like reachability, non-termination,
unboundedness are NP-complete for flat FIFO machines, generalizing similar
existing results for flat counter machines. We also show that reachability is
NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO
machines. We construct a trace-flattable system of many counter machines
communicating via rendez-vous that is bisimilar to a given flat FIFO machine,
which allows to model-check the original flat FIFO machine. Our results lay the
theoretical foundations and open the way to build a verification tool for
(general) FIFO machines based on analysis of flat sub-machines. |
| first_indexed | 2024-04-25T01:34:14Z |
| format | Article |
| id | doaj.art-2f04ec861fbf489a9fa1d88014193e29 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:14Z |
| publishDate | 2020-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-2f04ec861fbf489a9fa1d88014193e292024-03-08T10:32:05ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-10-01Volume 16, Issue 410.23638/LMCS-16(4:4)20205999Verification of Flat FIFO SystemsAlain FinkelM. PraveenThe decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.https://lmcs.episciences.org/5999/pdfcomputer science - computational complexitycomputer science - logic in computer sciencetheory of computation - parallel computing models |
| spellingShingle | Alain Finkel M. Praveen Verification of Flat FIFO Systems Logical Methods in Computer Science computer science - computational complexity computer science - logic in computer science theory of computation - parallel computing models |
| title | Verification of Flat FIFO Systems |
| title_full | Verification of Flat FIFO Systems |
| title_fullStr | Verification of Flat FIFO Systems |
| title_full_unstemmed | Verification of Flat FIFO Systems |
| title_short | Verification of Flat FIFO Systems |
| title_sort | verification of flat fifo systems |
| topic | computer science - computational complexity computer science - logic in computer science theory of computation - parallel computing models |
| url | https://lmcs.episciences.org/5999/pdf |
| work_keys_str_mv | AT alainfinkel verificationofflatfifosystems AT mpraveen verificationofflatfifosystems |