| 1. |
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Algorithmic Improvements in Regular Model Checking
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems, whose states can be represented as finite strings of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. In earlier papers, we have developed methods for computing the transitive closure (or the set of reachable states) of the transition relation, represented by a regular length-preserving transducer. In this paper, we present several improvements of these techniques, which reduce the size of intermediate approximations of the transitive closure: One improvement is to pre-process the transducer by \em bi-determinization, another is to use a more powerful equivalence relation for identifying histories (columns) of states in the transitive closure. We also present a simplified theoretical framework for showing soundness of the optimization, which is based on commuting simulations. The techniques have been implemented, and we report the speedups obtained from the respective optimizations.
|
|
| 3. |
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Better-Structured Transition Systems
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In automated verification of infinite-state systems, a variety of algorithms that operate on constraints representing sets of states have been developed. Many of these algorithms rely on well quasi-ordering of the constraint system for proving termination. A number of methods for generating new well quasi-ordered constraint systems have been proposed. However, many of these constraint systems suffer from constraint explosion as the number of constraints generated during analysis grows exponentially with the size of the problem. We suggest using the theory of better quasi-ordering to prove termination since that will allow generation of constraint systems that are less prone to constraint explosion. We also present a method to derive such constraint systems. We introduce existential zones, a constraint system for verification of systems with an unbounded number of clocks and use our methodology to prove that existential zones are better quasi-ordered. We show how to use existential zones in verification of timed Petri nets and present some experimental results. Finally, we present several other constraint systems which have been derived using our methodology.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
BQOs and Timed Petri Nets
- 2000
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In this paper, we use the theory of better quasi-orderings to define a methodology for inventing constraint systems which are both well quasi-ordered and compact. We apply our methodology by presenting new constraint systems for verification of systems with unboundedly many real-valued clocks, and use them for checking safety properties for lazy (non-urgent) timed Petri nets where each token is equipped with a real-valued clock.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Downward Closed Language Generators
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We use downward closed languages for representing sets of states when performing forward reachability analysis on infinite-state systems. Downward closed languages are often more succinct than exact representations of the set of reachable states. We introduce a formalism for representing downward closed languages, called downward closed language generators (dlgs). We show that standard set operations needed for performing symbolic reachability analysis are computable for dlgs. Using a class of hierarchically defined dlgs, we have implemented a prototype for analysing timed Petri nets and used it to analyze a parameterized version of Fischer's protocol. We also show how dlgs can be used for uniform representation of formalisms previously presented for models such as Petri nets and lossy channel systems.
|
|
| 7. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Forward Reachability Analysis of Timed Petri Nets
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for concurrent real-timed systems modelled by timed Petri nets, by performing symbolic forward reachability analysis. We introduce a formalism, called region generators for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions. Downward closed languages provide exact abstractions of sets of reachable states with respect to safety properties.We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples.We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol. We also used the tool to generate a finite-state abstraction of the protocol.
|
|
| 8. |
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Multi-Clock Timed Networks
- 2004
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider verification of safety properties for parameterized systems of timed processes, so called ıt timed networks. A timed network consists of a finite state process, called a controller, and an arbitrary set of identical timed processes. In a previous work, we showed that checking safety properties is decidable in the case where each timed process is equipped with a single real-valued clock. It was left open whether the result could be extended to multi-clock timed networks. We show that the problem becomes undecidable when each timed process has two clocks. On the other hand, we show that the problem is decidable when clocks range over a discrete time domain. This decidability result holds when processes have any finite number of clocks.
|
|
| 10. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Regular Model Checking for LTL(MSO)
- 2004
-
Ingår i: Proc. 16th Int. Conf. on Computer Aided Verification, LNCS.
-
Tidskriftsartikel (refereegranskat)
|
|
