1531. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification of time-sensitive models of ad hoc network protocols
- 2016
-
Ingår i: Theoretical Computer Science. - : Elsevier BV. - 0304-3975 .- 1879-2294. ; 612, s. 1-22
-
Tidskriftsartikel (refereegranskat)abstract
- We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.
|
|
1532. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Parameterized verification through view abstraction
- 2016
-
Ingår i: International Journal on Software Tools for Technology Transfer. - : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 18:5, s. 495-516
-
Tidskriftsartikel (refereegranskat)abstract
- We present a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees. Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue. We show that the method is complete for a large class of well quasi-ordered systems including Petri nets. Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.
|
|
1533. |
- Abdulla, Parosh Aziz, 1961-, et al.
(författare)
-
Parameterized verification under TSO is PSPACE-complete
- 2020
-
Ingår i: Proceedings of the ACM on Programming Languages. - New York, NY, USA : Association for Computing Machinery (ACM). - 2475-1421. ; 4:POPL, s. 26:1-26:29
-
Tidskriftsartikel (refereegranskat)abstract
- We consider parameterized verification of concurrent programs under the Total Store Order (TSO) semantics. A program consists of a set of processes that share a set of variables on which they can perform read and write operations. We show that the reachability problem for a system consisting of an arbitrary number of identical processes is PSPACE-complete. We prove that the complexity is reduced to polynomial time if the processes are not allowed to read the initial values of the variables in the memory. When the processes are allowed to perform atomic read-modify-write operations, the reachability problem has a non-primitive recursive complexity.
|
|
1534. |
|
|
1535. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Precise and sound automatic fence insertion procedure under PSO
- 2015
-
Ingår i: Networked Systems. - Cham : Springer. - 9783319268491 ; , s. 32-47
-
Konferensbidrag (refereegranskat)abstract
- We give a sound and complete procedure for fence insertion for concurrent finite-state programs running under the PSO memory model. This model allows ''write to read'' and ''write-to-write'' relaxations corresponding to the addition of an unbounded store buffers between processors and the main memory. We introduce a novel machine model, called the Hierarchical Single-Buffer (HSB) semantics, and show that the reachability problem for a program under PSO can be reduced to the reachability problem under HSB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure infers automatically a minimal set of fences that ensure correctness of the program. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples.
|
|
1536. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Priced timed Petri nets
- 2013
-
Ingår i: Logical Methods in Computer Science. - 1860-5974 .- 1860-5974. ; 9:4, s. 10:1-51
-
Tidskriftsartikel (refereegranskat)
|
|
1537. |
|
|
1538. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Push-down automata with gap-order constraints
- 2013
-
Ingår i: Fundamentals of Software Engineering. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642402128 ; , s. 199-216
-
Konferensbidrag (refereegranskat)
|
|
1539. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
R-automata
- 2008
-
Ingår i: CONCUR 2008 - Concurrency Theory. - Berlin : Springer-Verlag. - 9783540853602 ; , s. 67-81
-
Konferensbidrag (refereegranskat)abstract
- We introduce R-automata - finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. We define the language accepted by an R-automaton relative to a natural number D as the set of words allowing a run along which no counter value exceeds D. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number D such that the corresponding language is universal. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12] - a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Buchi acceptance conditions.
|
|
1540. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
R-automata
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce \emphR-automata – a model for analysis of systems with resources which are consumed in small parts but which can be replenished at once. An R-automaton is a finite state machine which operates on a finite number of unbounded counters (modeling the resources). The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. We define the language accepted by an R-automaton relative to a natural number D as the set of words allowing a run along which no counter value exceeds D. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number D such that the corresponding language is universal. The decidability proof is based on a reformulation of the problem in the language of finite monoids and solving it using the factorization forest theorem. This approach extends the way in which the factorization forest theorem was used to solve the limitedness problem for distance automata in Simon, 1994. We also show decidability of the non-emptiness problem and the limitedness problem, i.e., whether there is a natural number D such that the corresponding language is non-empty resp.\ all the accepted words can also be accepted with counter values smaller than D. Finally, we extend the decidability results to R-automata with Büchi acceptance conditions.
|
|