| 1. |
- Abdulla, Aziz, et al.
(författare)
-
Monotonic Abstraction : on Efficient Verification of Parameterized Systems
- 2009
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:5, s. 779-801
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Automatic verification of directory-based consistency protocols with graph constraints
- 2011
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 761-782
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a symbolic verification method for directory-based consistency protocols working for an arbitrary number of controlled resources and competing processes. We use a graph-based language to specify in a uniform way both client/server interaction schemes and manipulation of directories that contain the access rights of individual clients. Graph transformations model the dynamics of a given protocol. Universally quantified conditions defined on the labels of edges incident to a given node are used to model inspection of directories, invalidation loops and integrity conditions. Our verification procedure computes an approximated backward reachability analysis by using a symbolic representation of sets of configurations. Termination is ensured by using the theory of well-quasi orderings.
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Bisimulation minimization of tree automata
- 2007
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 18:4, s. 699-713
-
Tidskriftsartikel (refereegranskat)abstract
- We extend an algorithm by Paige and Tarjan that solves the coarsest stable refinement problem to the domain of trees. The algorithm is used to minimize nondeterministic tree automata (NTA) with respect to bisimulation. We show that our algorithm has an overall complexity of $O(\hat{r} m \log n)$, where $\hat{r}$ is the maximum rank of any symbol in the input alphabet, m is the total size of the transition table, and n is the number of states.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Bisimulation minimization of tree automata
- 2007
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 18:4, s. 699-713
-
Tidskriftsartikel (refereegranskat)
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Composed bisimulation for tree automata
- 2009
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 20:4, s. 685-700
-
Tidskriftsartikel (refereegranskat)
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Monotonic abstraction for programs with multiply-linked structures
- 2013
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 24:2, s. 187-210
-
Tidskriftsartikel (refereegranskat)abstract
- We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.
|
|
| 7. |
- Adamaszek, Anna, et al.
(författare)
-
PTAS for k-tour cover poblem on the plane for moderately large values of k
- 2010
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 21:6, s. 893-904
-
Tidskriftsartikel (refereegranskat)abstract
- Let P be a set of n points in the Euclidean plane and let O be the origin point in the plane. In the k-tour cover problem (called frequently the capacitated vehicle routing problem), the goal is to minimize the total length of tours that cover all points in P, such that each tour starts and ends in O and covers at most k points from P. The k-tour cover problem is known to be NP-hard. It is also known to admit constant factor approximation algorithms for all values of k and even a polynomial-time approximation scheme (PTAS) for small values of k, k = circle divide (log n/ log log n). In this paper, we significantly enlarge the set of values of k for which a PTAS is provable. We present a new PTAS for all values of k <= 2(log delta n), where delta = delta(epsilon). The main technical result proved in the paper is a novel reduction of the k-tour cover problem with a set of n points to a small set of instances of the problem, each with circle divide((k/epsilon)(circle divide(1))) points.
|
|
| 8. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
Adjacent Ordered Multi-Pushdown Systems
- 2014
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 25:8, s. 1083-1096
-
Tidskriftsartikel (refereegranskat)abstract
- Multi-pushdown systems are formal models of multi-threaded programs. As they are Turing powerful in their full generality, several decidable subclasses, constituting under-approximations of the original system, have been studied in the recent years. Ordered Multi-Pushdown Systems (OMPDSs) impose an order on the stacks and limit pop actions to the lowest non-empty stack. The control state reachability for OMPDSs is 2-ETIME-COMPLETE. We propose a restriction on OMPDSs, called Adjacent OMPDSs (AOMPDS), where values may be pushed only on the lowest non-empty stack or one of its two neighbours. We describe EXPTIME decision procedures for reachability and LTL model-checking and establish matching lower bounds. We demonstrate the utility of this model as an algorithmic tool via optimal reductions from other models.
|
|
| 9. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete
- 2017
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 28:8, s. 945-975
-
Tidskriftsartikel (refereegranskat)abstract
- We consider ordered multi-pushdown automata, a multi-stack extension of pushdown automata that comes with a constraint on stack operations: a pop can only be performed on the first non-empty stack (which implies that we assume a linear ordering on the collection of stacks). We show that the emptiness problem for multi-pushdown automata is 2ETIME-complete. Containment in 2ETIME is shown by translating an automaton into a grammar for which we can check if the generated language is empty. The lower bound is established by simulating the behavior of an alternating Turing machine working in exponential space. We also compare ordered multi-pushdown automata with the model of bounded-phase (visibly) multi-stack pushdown automata, which do not impose an ordering on stacks, but restrict the number of alternations of pop operations on different stacks.
|
|
| 10. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
On Yen's path logic for Petri nets
- 2011
-
Ingår i: International Journal of Foundations of Computer Science. - 0129-0541. ; 22:4, s. 783-799
-
Tidskriftsartikel (refereegranskat)
|
|
