arXiv subjects

Mohamed Faouzi Atig

Publications and source records attributed to Mohamed Faouzi Atig.

32 records · Page 2Linked to original sources

arXiv2018

Communicating Timed Processes with Perfect Timed Channels

We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the finite-state processes are replaced by timed automata, and messages inside the perfect channels are equipped with clocks representing their ages. In addition to the standard operations (resetting clocks, checking guards of clocks) each automaton can either (1) append a message to the tail of a channel with an initial age or (2) receive the message at the head of a channel if its age satisfies a set of given constraints. In this paper, we show that the reachability problem is undecidable even in the case of two timed automata connected by one unidirectional timed channel if one allows global clocks (that the two automata can check and manipulate). We prove that this undecidability still holds even for CTA consisting of three timed automata and two unidirectional timed channels (and without any global clock). However, the reachability problem becomes decidable (in $\mathsf{EXPTIME}$) in the case of two automata linked with one unidirectional timed channel and with no global clock. Finally, we consider the bounded-context case, where in each context, only one timed automaton is allowed to receive messages from one channel while being able to send messages to all the other timed channels. In this case we show that the reachability problem is decidable.

cs.FL↗

arXiv2018

A Load-Buffer Semantics for Total Store Ordering

We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (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 the 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 semantics that is more amenable to efficient algorithmic verification and for the 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 obtaining 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.

cs.FL↗

arXiv2018

Mending Fences with Self-Invalidation and Self-Downgrade

Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.

cs.LO↗

arXiv2016

Stateless Model Checking for POWER

We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to an axiomatic model of POWER. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.

cs.LO↗

arXiv2016

Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version)

We propose a formalism to model database-driven systems, called database manipulating systems (DMS). The actions of a DMS modify the current instance of a relational database by adding new elements into the database, deleting tuples from the relations and adding tuples to the relations. The elements which are modified by an action are chosen by (full) first-order queries. DMS is a highly expressive model and can be thought of as a succinct representation of an infinite state relational transition system, in line with similar models proposed in the literature. We propose monadic second order logic (MSO-FO) to reason about sequences of database instances appearing along a run. Unsurprisingly, the linear-time model checking problem of DMS against MSO-FO is undecidable. Towards decidability, we propose under-approximate model checking of DMS, where the under-approximation parameter is the "bound on recency". In a $k$-recency-bounded run, only the most recent $k$ elements in the current active domain may be modified by an action. More runs can be verified by increasing the bound on recency. Our main result shows that recency-bounded model checking of DMS against MSO-FO is decidable, by a reduction to the satisfiability problem of MSO over nested words.

cs.DB↗

arXiv2016

Complexity of regular abstractions of one-counter languages

We study the computational and descriptional complexity of the following transformation: Given a one-counter automaton (OCA) A, construct a nondeterministic finite automaton (NFA) B that recognizes an abstraction of the language L(A): its (1) downward closure, (2) upward closure, or (3) Parikh image. For the Parikh image over a fixed alphabet and for the upward and downward closures, we find polynomial-time algorithms that compute such an NFA. For the Parikh image with the alphabet as part of the input, we find a quasi-polynomial time algorithm and prove a completeness result: we construct a sequence of OCA that admits a polynomial-time algorithm iff there is one for all OCA. For all three abstractions, it was previously unknown if appropriate NFA of sub-exponential size exist.

cs.FL↗

arXiv2014

Infinite-State Energy Games

Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata. Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

cs.GT↗

arXiv2014

Zenoness for Timed Pushdown Automata

Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clocks and the age of the topmost symbol. Therefore, dense-timed pushdown automata subsume both pushdown automata and timed automata. We have previously shown that the reachability problem for this model is decidable. In this paper, we study the zenoness problem and show that it is EXPTIME-complete.

cs.FL↗

arXiv2013

Proceedings 14th International Workshop on Verification of Infinite-State Systems

This volume contains the proceedings of Infinity'12, the 14th International Workshop on Verification of Infinite-State Systems, which was held in Paris, France on the 27th of August 2012 as a satellite event of FM'12. The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

cs.LO↗

arXiv2012

Adding Time to Pushdown Automata

In this tutorial, we illustrate through examples how we can combine two classical models, namely those of pushdown automata (PDA) and timed automata, in order to obtain timed pushdown automata (TPDA). Furthermore, we describe how the reachability problem for TPDAs can be reduced to the reachability problem for PDAs.

cs.LO↗

arXiv2012

Model-Checking of Ordered Multi-Pushdown Automata

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

cs.LO↗

arXiv2012

Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard

We address the model checking problem for shared memory concurrent programs modeled as multi-pushdown systems. We consider here boolean programs with a finite number of threads and recursive procedures. It is well-known that the model checking problem is undecidable for this class of programs. In this paper, we investigate the decidability and the complexity of this problem under the assumption of bounded context-switching defined by Qadeer and Rehof, and of phase-boundedness proposed by La Torre et al. On the model checking of such systems against temporal logics and in particular branching time logics such as the modal $μ$-calculus or CTL has received little attention. It is known that parity games, which are closely related to the modal $μ$-calculus, are decidable for the class of bounded-phase systems (and hence for bounded-context switching as well), but with non-elementary complexity (Seth). A natural question is whether this high complexity is inevitable and what are the ways to get around it. This paper addresses these questions and unfortunately, and somewhat surprisingly, it shows that branching model checking for MPDSs is inherently an hard problem with no easy solution. We show that parity games on MPDS under phase-bounding restriction is non-elementary. Our main result shows that model checking a $k$ context bounded MPDS against a simple fragment of CTL, consisting of formulas that whose temporal operators come from the set ${\EF, \EX}$, has a non-elementary lower bound.

cs.LO↗

arXiv2012

Approximating Petri Net Reachability Along Context-free Traces

We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) 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.

cs.FL↗

arXiv2011

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads

Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis explores all behaviors of a concurrent program up to some fixed number of context switches between threads. This definition is inadequate for programs that create threads dynamically because bounding the number of context switches in a computation also bounds the number of threads involved in the computation. In this paper, we propose a more general definition of context-bounded analysis useful for programs with dynamic thread creation. The idea is to bound the number of context switches for each thread instead of bounding the number of switches of all threads. We consider several variants based on this new definition, and we establish decidability and complexity results for the analysis induced by them.

cs.LO↗