Search Results

Documents authored by Atig, Mohamed Faouzi

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.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.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.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.2018.15
Verifying Quantitative Temporal Properties of Procedural Programs

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
We address the problem of specifying and verifying quantitative properties of procedural programs. These properties typically involve constraints on the relative cumulated costs of executing various tasks (by invoking for instance some particular procedures) within the scope of the execution of some particular procedure. An example of such properties is "within the execution of each invocation of procedure P, the time spent in executing invocations of procedure Q is less than 20 % of the total execution time". We introduce specification formalisms, both automata-based and logic-based, for expressing such properties, and we study the links between these formalisms and their application in model-checking. On one side, we define Constrained Pushdown Systems (CPDS), an extension of pushdown systems with constraints, expressed in Presburger arithmetics, on the numbers of occurrences of each symbol in the alphabet within invocation intervals (subcomputations between matching pushes and pops), and on the other side, we introduce a higher level specification language that is a quantitative extension of CaRet (the Call-Return temporal logic) called QCaRet where nested quantitative constraints over procedure invocation intervals are expressible using Presburger arithmetics. Then, we investigate (1) the decidability of the reachability and repeated reachability problems for CPDS, and (2) the effective reduction of the model-checking problem of procedural programs (modeled as visibly pushdown systems) against QCaRet formulas to these problems on CPDS.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verifying Quantitative Temporal Properties of Procedural Programs. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.CONCUR.2018.15,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Verifying Quantitative Temporal Properties of Procedural Programs}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{15:1--15:17},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.15},
  URN =		{urn:nbn:de:0030-drops-95531},
  doi =		{10.4230/LIPIcs.CONCUR.2018.15},
  annote =	{Keywords: Verification, Formal Methods, Pushdown systems, Visibly pushdown, Quantitative Temporal Properties}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.11
Verification of Asynchronous Programs with Nested Locks

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
In this paper, we consider asynchronous programs consisting of multiple recursive threads running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronise through a finite set of locks. In this paper, we show that the reachability problem for such class of asynchronous programs is undecidable even under the nested locking policy. We then show that the reachability problem becomes decidable (Exp-space-complete) when the locks are not allowed to be held across tasks. Finally, we show that the problem is NP-complete when in addition to previous restrictions, threads always read tasks from the same state.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. Verification of Asynchronous Programs with Nested Locks. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2017.11,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{Verification of Asynchronous Programs with Nested Locks}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{11:1--11:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.11},
  URN =		{urn:nbn:de:0030-drops-84106},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.11},
  annote =	{Keywords: asynchronous programs locks concurrency multi-set pushdown systems, multi-threaded programs, reachability, model checking, verification, nested lockin}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.49
On the Upward/Downward Closures of Petri Nets

Authors: Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward closures, we prove that the size of the minimal automata can be non-primitive recursive. In the case of BPP nets, a well-known subclass of Petri nets, we show that an FSA accepting the downward/upward closure can be constructed in exponential time. Furthermore, we consider the problem of checking whether a simple regular language is included in the downward/upward closure of a Petri net/BPP net language. We show that this problem is EXPSPACE-complete (resp. NP-complete) in the case of Petri nets (resp. BPP nets). Finally, we show that it is decidable whether a Petri net language is upward/downward closed.
Cite as

Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan. On the Upward/Downward Closures of Petri Nets. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 49:1-49:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.MFCS.2017.49,
  author =	{Atig, Mohamed Faouzi and Meyer, Roland and Muskalla, Sebastian and Saivasan, Prakash},
  title =	{{On the Upward/Downward Closures of Petri Nets}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{49:1--49:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.49},
  URN =		{urn:nbn:de:0030-drops-81278},
  doi =		{10.4230/LIPIcs.MFCS.2017.49},
  annote =	{Keywords: Petri nets, BPP nets, downward closure, upward closure}
}
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.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.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.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
DOI: 10.4230/LIPIcs.FSTTCS.2014.611
On Bounded Reachability Analysis of Shared Memory Systems

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan

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

Abstract
This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results.
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 611-623, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2014.611,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Narayan Kumar, K. and Saivasan, Prakash},
  title =	{{On Bounded Reachability Analysis of Shared Memory Systems}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{611--623},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.611},
  URN =		{urn:nbn:de:0030-drops-48754},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.611},
  annote =	{Keywords: Reachability problem, Pushdown systems, Counter 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.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.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.2011.152
Approximating Petri Net Reachability Along Context-free Traces

Authors: Mohamed Faouzi Atig and Pierre Ganty

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

Abstract
We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) (with reachability as acceptance condition) is empty. Our contribution to solve this long-standing problem which relates, for instance, to the reachability analysis of recursive programs over unbounded data domain, is to identify a class of CFLs called the finite-index CFLs for which the problem is decidable. The k-index approximation of a CFL can be obtained by discarding all the words that cannot be derived within a budget k on the number of occurrences of non-terminals. A finite-index CFL is thus a CFL which coincides with its k-index approximation for some k. We decide whether the intersection of a finite-index CFL and a PNL is empty by reducing it to the reachability problem of Petri nets with weak inhibitor arcs, a class of systems with infinitely many states for which reachability is known to be decidable. Conversely, we show that the reachability problem for a Petri net with weak inhibitor arcs reduces to the emptiness problem of a finite-index CFL intersected with a PNL.
Cite as

Mohamed Faouzi Atig and Pierre Ganty. Approximating Petri Net Reachability Along Context-free Traces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 152-163, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2011.152,
  author =	{Atig, Mohamed Faouzi and Ganty, Pierre},
  title =	{{Approximating Petri Net Reachability Along Context-free Traces}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{152--163},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.152},
  URN =		{urn:nbn:de:0030-drops-33448},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.152},
  annote =	{Keywords: Petri nets, Context-free Grammars, Reachability Problem}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.216
Global Model Checking of Ordered Multi-Pushdown Systems

Authors: Mohamed Faouzi Atig

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

Abstract
In this paper, we address the verification problem of ordered multi-pushdown systems: A multi-stack extension of pushdown systems that comes with a constraint on stack operations such that a pop can only be performed on the first non-empty stack. First, we show that for an ordered multi-pushdown system the set of all predecessors of a regular set of configurations is an effectively constructible regular set. Then, we exploit this result to solve the global model checking which consists in computing the set of all configurations of an ordered multi-pushdown system that satisfy a given $w$-regular property (expressible in linear-time temporal logics or the linear-time $\mu$-calculus). As an immediate consequence of this result, we obtain an 2ETIME upper bound for the model checking problem of $w$-regular properties for ordered multi-pushdown systems (matching its lower-bound).
Cite as

Mohamed Faouzi Atig. Global Model Checking of Ordered Multi-Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 216-227, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{atig:LIPIcs.FSTTCS.2010.216,
  author =	{Atig, Mohamed Faouzi},
  title =	{{Global  Model Checking of Ordered Multi-Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{216--227},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.216},
  URN =		{urn:nbn:de:0030-drops-28653},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.216},
  annote =	{Keywords: Concurrent Programs, Pushdown Systems, Global Model-Checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1739
Analyzing Asynchronous Programs with Preemption

Authors: Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili

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

Abstract
Multiset pushdown systems have been introduced by Sen and Viswanathan as an adequate model for asynchronous programs where some procedure calls can be stored as tasks to be processed later. The model is a pushdown system supplied with a multiset of pending tasks. Tasks may be added to the multiset at each transition, whereas a task is taken from the multiset only when the stack is empty. In this paper, we consider an extension of these models where tasks may be of different priority level, and can be preempted at any point of their execution by tasks of higher priority. We investigate the control point reachability problem for these models. Our main result is that this problem is decidable by reduction to the reachability problem for a decidable class of Petri nets with inhibitor arcs. We also identify two subclasses of these models for which the control point reachability problem is reducible respectively to the reachability problem and to the coverability problem for Petri nets (without inhibitor arcs).
Cite as

Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. Analyzing Asynchronous Programs with Preemption. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 37-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{atig_et_al:LIPIcs.FSTTCS.2008.1739,
  author =	{Atig, Mohamed Faouzi and Bouajjani, Ahmed and Touili, Tayssir},
  title =	{{Analyzing Asynchronous  Programs with Preemption}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{37--48},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1739},
  URN =		{urn:nbn:de:0030-drops-17398},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1739},
  annote =	{Keywords: Multiset Pushdown Systems, Multithreaded Asynchronous Programs, Program verification, Verification algorithms}
}
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