18 Search Results for "Abdulla, Parosh A."

Document
DOI: 10.4230/LIPIcs.CSL.2024.46
Concurrent Stochastic Lossy Channel Games

Authors: Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.
Cite as

Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla. Concurrent Stochastic Lossy Channel Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 46:1-46:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{stan_et_al:LIPIcs.CSL.2024.46,
  author =	{Stan, Daniel and Najib, Muhammad and Lin, Anthony Widjaja and Abdulla, Parosh Aziz},
  title =	{{Concurrent Stochastic Lossy Channel Games}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{46:1--46:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.46},
  URN =		{urn:nbn:de:0030-drops-196894},
  doi =		{10.4230/LIPIcs.CSL.2024.46},
  annote =	{Keywords: concurrent, games, stochastic, lossy channels, wqo, finite attractor property, cooperative, core, Nash equilibrium}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.3
Inclusion Testing of Büchi Automata Based on Well-Quasiorders

Authors: Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.
Cite as

Kyveli Doveri, Pierre Ganty, Francesco Parolini, and Francesco Ranzato. Inclusion Testing of Büchi Automata Based on Well-Quasiorders. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doveri_et_al:LIPIcs.CONCUR.2021.3,
  author =	{Doveri, Kyveli and Ganty, Pierre and Parolini, Francesco and Ranzato, Francesco},
  title =	{{Inclusion Testing of B\"{u}chi Automata Based on Well-Quasiorders}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{3:1--3:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.3},
  URN =		{urn:nbn:de:0030-drops-143802},
  doi =		{10.4230/LIPIcs.CONCUR.2021.3},
  annote =	{Keywords: B\"{u}chi (Pushdown) Automata, \omega-Language Inclusion, Well-quasiorders}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.16
On the Separability Problem of String Constraints

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We address the separability problem for straight-line string constraints. The separability problem for languages of a class C by a class S asks: given two languages A and B in C, does there exist a language I in S separating A and B (i.e., I is a superset of A and disjoint from B)? The separability of string constraints is the same as the fundamental problem of interpolation for string constraints. We first show that regular separability of straight line string constraints is undecidable. Our second result is the decidability of the separability problem for straight-line string constraints by piece-wise testable languages, though the precise complexity is open. In our third result, we consider the positive fragment of piece-wise testable languages as a separator, and obtain an ExpSpace algorithm for the separability of a useful class of straight-line string constraints, and a Pspace-hardness result.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. On the Separability Problem of String Constraints. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2020.16,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Dave, Vrunda and Krishna, Shankara Narayanan},
  title =	{{On the Separability Problem of String Constraints}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{16:1--16:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.16},
  URN =		{urn:nbn:de:0030-drops-128286},
  doi =		{10.4230/LIPIcs.CONCUR.2020.16},
  annote =	{Keywords: string constraints, separability, interpolants}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.8
Verification of Timed Asynchronous Programs

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
In this paper, we address the verification problem for timed asynchronous programs. We associate to each task, a deadline for its execution. We first show that the control state reachability problem for such class of systems is decidable while the configuration reachability problem is undecidable. Then, we consider the subclass of timed asynchronous programs where tasks are always being executed from the same state. For this subclass, we show that the control state reachability problem is PSPACE-complete. Furthermore, we show the decidability for the configuration reachability problem for the subclass.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya. Verification of Timed Asynchronous Programs. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2018.8,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Krishna, Shankara Narayanan and Vaidya, Shaan},
  title =	{{Verification of Timed Asynchronous Programs}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.8},
  URN =		{urn:nbn:de:0030-drops-99076},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.8},
  annote =	{Keywords: Reachability, Timed Automata, Asynchronous programs}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.6
Universal Safety for Timed Petri Nets is PSPACE-complete

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network. This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number m of tokens, such that starting with m tokens in a given place, and none in the other places, some given transition is eventually enabled. We show that these problems are PSPACE-complete.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2018.6,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Ciobanu, Radu and Mayr, Richard and Totzke, Patrick},
  title =	{{Universal Safety for Timed Petri Nets is PSPACE-complete}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{6:1--6:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.6},
  URN =		{urn:nbn:de:0030-drops-95447},
  doi =		{10.4230/LIPIcs.CONCUR.2018.6},
  annote =	{Keywords: timed networks, safety checking, Petri nets, coverability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.38
Data Multi-Pushdown Automata

Authors: Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We extend the classical model of multi-pushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gap-order constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number. It is well-known that the verification of any non-trivial property of multi-pushdown systems is undecidable, even for two stacks and for a finite data-domain. In this paper, we show the decidability of the reachability problem for the classes of data multi-pushdown system that admit a bounded split-width (or equivalently a bounded tree-width). As an immediate consequence, we obtain decidability for several subclasses of data multi-pushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.
Cite as

Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data Multi-Pushdown Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2017.38,
  author =	{Abdulla, Parosh Aziz and Aiswarya, C. and Atig, Mohamed Faouzi},
  title =	{{Data Multi-Pushdown Automata}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.38},
  URN =		{urn:nbn:de:0030-drops-78049},
  doi =		{10.4230/LIPIcs.CONCUR.2017.38},
  annote =	{Keywords: Pushdown Systems, Model-Checking, Gap-Order, Bounded Split-Width}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.5
The Benefits of Duality in Verifying Concurrent Programs under TSO

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
We address the problem of verifying safety properties of concurrent programs running over the TSO memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO model that is more amenable for efficient algorithmic verification and for extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows to obtain a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. The Benefits of Duality in Verifying Concurrent Programs under TSO. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2016.5,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Ngo, Tuan Phong},
  title =	{{The Benefits of Duality in Verifying Concurrent Programs under TSO}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.5},
  URN =		{urn:nbn:de:0030-drops-61710},
  doi =		{10.4230/LIPIcs.CONCUR.2016.5},
  annote =	{Keywords: Weak Memory Models, Reachability Problem, Parameterized Systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.192
What's Decidable about Availability Languages?

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
We study here the algorithmic analysis of systems modeled in terms of availability languages. Our first main result is a positive answer to the emptiness problem: it is decidable whether a given availability language contains a word. The key idea is an inductive construction that replaces availability languages with Parikh-equivalent regular languages. As a second contribution, we solve the intersection problem modulo bounded languages: given availability languages and a bounded language, it is decidable whether the intersection of the former contains a word from the bounded language. We show that the problem is NP-complete. The idea is to reduce to satisfiability of existential Presburger arithmetic. Since the (general) intersection problem for availability languages is known to be undecidable, our results characterize the decidability border for this model. Our last contribution is a study of the containment problem between regular and availability languages. We show that safety verification, i.e., checking containment of an availability language in a regular language, is decidable. The containment problem of regular languages in availability languages is proven undecidable.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What's Decidable about Availability Languages?. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 192-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2015.192,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Meyer, Roland and Seyed Salehi, Mehdi},
  title =	{{What's Decidable about Availability Languages?}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{192--205},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.192},
  URN =		{urn:nbn:de:0030-drops-56602},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.192},
  annote =	{Keywords: Availability, formal languages, emptiness, decidability}
}
Document
Invited Paper
DOI: 10.4230/OASIcs.SynCoP.2015.1
View Abstraction – A Tutorial (Invited Paper)

Authors: Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical Burns' mutual exclusion protocol.
Cite as

Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík. View Abstraction – A Tutorial (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:OASIcs.SynCoP.2015.1,
  author =	{Abdulla, Parosh A. and Haziza, Fr\'{e}deric and Hol{\'\i}k, Luk\'{a}\v{s}},
  title =	{{View Abstraction – A Tutorial}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{1--15},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.1},
  URN =		{urn:nbn:de:0030-drops-56057},
  doi =		{10.4230/OASIcs.SynCoP.2015.1},
  annote =	{Keywords: program verification, model checking, parameterized systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.653
Verification of Dynamic Register Automata

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We consider the verification problem for Dynamic Register Automata (DRA). DRA extend classical register automata by process creation. In this setting, each process is equipped with a finite set of registers in which the process IDs of other processes can be stored. A process can communicate with processes whose IDs are stored in its registers and can send them the content of its registers. The state reachability problem asks whether a DRA reaches a configuration where at least one process is in an error state. We first show that this problem is in general undecidable. This result holds even when we restrict the analysis to configurations where the maximal length of the simple paths in their underlying (un)directed communication graphs are bounded by some constant. Then we introduce the model of degenerative DRA which allows non-deterministic reset of the registers. We prove that for every given DRA, its corresponding degenerative one has the same set of reachable states. While the state reachability of a degenerative DRA remains undecidable, we show that the problem becomes decidable with nonprimitive recursive complexity when we restrict the analysis to strongly bounded configurations, i.e. configurations whose underlying undirected graphs have bounded simple paths. Finally, we consider the class of strongly safe DRA, where all the reachable configurations are assumed to be strongly bounded. We show that for strongly safe DRA, the state reachability problem becomes decidable.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. Verification of Dynamic Register Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 653-665, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2014.653,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Kara, Ahmet and Rezine, Othmane},
  title =	{{Verification of  Dynamic Register Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{653--665},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.653},
  URN =		{urn:nbn:de:0030-drops-48787},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.653},
  annote =	{Keywords: Verification, Reachability problem, Register automata}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.374
Timed Lossy Channel Systems

Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
Lossy channel systems are a classical model with applications ranging from the modeling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this paper, we extend the model by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of Timed Lossy Channel Systems (TLCS). The main contribution of the paper is to show that the control state reachability problem is decidable for TLCS.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Timed Lossy Channel Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 374-386, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2012.374,
  author =	{Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Cederberg, Jonathan},
  title =	{{Timed Lossy Channel Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{374--386},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.374},
  URN =		{urn:nbn:de:0030-drops-38746},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.374},
  annote =	{Keywords: Lossy channel systems, timed automata, model checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2009.2302
Mediating for Reduction (on Minimizing Alternating Büchi Automata)

Authors: Parosh A. Abdulla, Yu-Fang Chen, Lukas Holik, and Tomas Vojnar

Published in: LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

Abstract
We propose a new approach for minimizing alternating B\"uchi automata (ABA). The approach is based on the so called \emph{mediated equivalence} on states of ABA, which is the maximal equivalence contained in the so called \emph{mediated preorder}. Two states $p$ and $q$ can be related by the mediated preorder if there is a~\emph{mediator} (mediating state) which forward simulates $p$ and backward simulates $q$. Under some further conditions, letting a computation on some word jump from $q$ to $p$ (due to they get collapsed) preserves the language as the automaton can anyway already accept the word without jumps by runs through the mediator. We further show how the mediated equivalence can be computed efficiently. Finally, we show that, compared to the standard forward simulation equivalence, the mediated equivalence can yield much more significant reductions when applied within the process of complementing B\"uchi automata where ABA are used as an intermediate model.
Cite as

Parosh A. Abdulla, Yu-Fang Chen, Lukas Holik, and Tomas Vojnar. Mediating for Reduction (on Minimizing Alternating Büchi Automata). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2009.2302,
  author =	{Abdulla, Parosh A. and Chen, Yu-Fang and Holik, Lukas and Vojnar, Tomas},
  title =	{{Mediating for Reduction (on Minimizing Alternating B\"{u}chi Automata)}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{1--12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Kannan, Ravi and Narayan Kumar, K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2302},
  URN =		{urn:nbn:de:0030-drops-23027},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2302},
  annote =	{Keywords: Alternating Automata, Buchi Automata, Automata Minimization, Buchi Automata Complementation, Simulation Preorder, forward and backward simulation, mediated equivalence}
}
Document
DOI: 10.4230/DagSemProc.08171.3
Shape Analysis via Monotonic Abstraction

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, and Ahmed Rezine

Published in: Dagstuhl Seminar Proceedings, Volume 8171, Beyond the Finite: New Challenges in Verification and Semistructured Data (2008)

Abstract
We propose a new formalism for reasoning about dynamic memory heaps, using monotonic abstraction and symbolic backward reachability analysis. We represent the heaps as graphs, and introduce an ordering on these graphs. This enables us to represent the violation of a given safety property as the reachability of a finitely representable set of bad graphs. We also describe how to symbolically compute the reachable states in the transition system induced by a program.
Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, and Ahmed Rezine. Shape Analysis via Monotonic Abstraction. In Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, Volume 8171, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{azizabdulla_et_al:DagSemProc.08171.3,
  author =	{Aziz Abdulla, Parosh and Bouajjani, Ahmed and Cederberg, Jonathan and Haziza, Fr\'{e}d\'{e}ric and Ji, Ran and Rezine, Ahmed},
  title =	{{Shape Analysis via Monotonic Abstraction}},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8171},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha\"{e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.08171.3},
  URN =		{urn:nbn:de:0030-drops-15590},
  doi =		{10.4230/DagSemProc.08171.3},
  annote =	{Keywords: Shape analysis, Program verification, Static analysis}
}
Document
DOI: 10.4230/DagSemProc.06081.2
06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis

Authors: Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
{\em Software systems} are present at the very heart of many daily-life applications, such as in communication (telephony and mobile Internet), transportation, energy, health, etc. Such systems are very often {\em critical}\/ in the sense that their failure can have considerable human/economical consequences. In order to ensure reliability, development methods must include {\em algorithmic analysis and verification techniques} which allow (1) to detect automatically defective behaviors of the system and to analyze their source, and (2) to check that every component of a system conforms to its specification. Two important and quite active research communities are particularly concerned with this challenge: the community of computer-aided verification, especially the community of (infinite-state) model checking, and the community of static program analysis. From 19.02.06 to 24.02.06, 51 researchers from these two communities met at the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' in order to improve and deepen the mutual understanding of the developed technologies and to trigger collaborations. During the seminar which was held at the International Conference and Research Center (IBFI), Schloss Dagstuhl, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar are put together in this paper.
Cite as

Parosh Aziz Abdulla, Ahmed Bouajjani, and Markus Müller-Olm. 06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:DagSemProc.06081.2,
  author =	{Abdulla, Parosh Aziz and Bouajjani, Ahmed and M\"{u}ller-Olm, Markus},
  title =	{{06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.2},
  URN =		{urn:nbn:de:0030-drops-7973},
  doi =		{10.4230/DagSemProc.06081.2},
  annote =	{Keywords: Infinite-state systems, model checking, program analysis, software verification}
}
Document
DOI: 10.4230/DagSemProc.06081.3
Analysis of Dynamic Communicating Systems by Hierarchical Abstraction

Authors: Jörg Bauer and Reinhard Wilhelm

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract
We propose a new abstraction technique for verifying topology properties of dynamic communicating systems (DCS), a special class of infinite-state systems. DCS are characterized by unbounded creation and destruction of objects along with an evolving communication connectivity or topology. We employ a lightweight graph transformation system to specify DCS. Hierarchical Abstraction (HA) computes a bounded over-approximation of all topologies that can occur in a DCS directly from its transformation rules. HA works in two steps. First, for each connected component, called cluster, of a topology, objects sharing a common property are summarized to one abstract object. Then isomorphic abstract connected components are summarized to one abstract component, called abstract cluster. This yields a conservative approximation of all graphs that may occur during any DCS run. The technique is implemented.
Cite as

Jörg Bauer and Reinhard Wilhelm. Analysis of Dynamic Communicating Systems by Hierarchical Abstraction. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bauer_et_al:DagSemProc.06081.3,
  author =	{Bauer, J\"{o}rg and Wilhelm, Reinhard},
  title =	{{Analysis of Dynamic Communicating Systems by Hierarchical Abstraction}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--25},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.3},
  URN =		{urn:nbn:de:0030-drops-7271},
  doi =		{10.4230/DagSemProc.06081.3},
  annote =	{Keywords: Graph transformation, Abstract Interpretation, Shape Analysis}
}
  • Refine by Author
  • 10 Abdulla, Parosh Aziz
  • 8 Atig, Mohamed Faouzi
  • 4 Bouajjani, Ahmed
  • 2 Abdulla, Parosh A.
  • 2 Cederberg, Jonathan
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Verification by model checking
  • 1 Security and privacy → Logic and verification
  • 1 Theory of computation
  • 1 Theory of computation → Concurrency
  • Show More...

  • Refine by Keyword
  • 3 model checking
  • 2 Shape analysis
  • 1 Abstract Interpretation
  • 1 Acceleration
  • 1 Alternating Automata
  • Show More...

  • Refine by Type
  • 18 document

  • Refine by Publication Year
  • 5 2006
  • 2 2015
  • 2 2018
  • 1 2008
  • 1 2009
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact