| 1. |
|
|
| 2. |
- 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.
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Bisimulation minimization of tree automata
- 2006
-
Ingår i: Implementation and Application of Automata. ; , s. 699-713
-
Konferensbidrag (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 ((r) over cap log n), where (r) over cap 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)
-
Bisimulation Minimization of Tree Automata
- 2006
-
Ingår i: Implementation and Application of Automata. - Berlin : Springer-Verlag. ; , s. 173-185
-
Konferensbidrag (refereegranskat)
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Composed Bisimulation for Tree Automata
- 2008
-
Ingår i: Implementation and Application of Automata. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783540708438 ; , s. 212-222
-
Konferensbidrag (refereegranskat)
|
|
| 7. |
- 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)
|
|
| 8. |
|
|
| 9. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
- 2007
-
Ingår i: Logical Methods in Computer Science. - 1860-5974 .- 1860-5974. ; 3:1, s. 1-61
-
Tidskriftsartikel (refereegranskat)abstract
- We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs. (i) Zenoness: whether there exists a zeno-computation from a given marking, i.e., an infinite computation which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from [Escrig et al.]. Furthermore, the related question if there exist arbitrarily fast computations from a given marking is also decidable. On the other hand, universal zenoness, i.e., the question if all infinite computations from a given marking are zeno, is undecidable. (ii) Token liveness: whether a token is alive in a marking, i.e., whether there is a computation from the marking which eventually consumes the token. We show decidability of the problem by reducing it to the coverability problem, which is decidable for TPNs. (iii) Boundedness: whether the size of the reachable markings is bounded. We consider two versions of the problem; namely semantic boundedness where only live tokens are taken into consideration in the markings, and syntactic boundedness where also dead tokens are considered. We show undecidability of semantic boundedness, while we prove that syntactic boundedness is decidable through an extension of the Karp-Miller algorithm.
|
|
| 10. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Eager Markov Chains
- 2006
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We consider infinite-state discrete Markov chains which are \empheager: the probability of avoiding a defined set of final states for more than n steps decreases exponentially in n. We study the problem of computing the expected reward (or cost) of runs until reaching the final states, where rewards are assigned to individual runs by computable reward functions. We present a path exploration scheme, based on forward reachability analysis, to approximate the expected reward up-to an arbitrarily small error, and show that the scheme is guaranteed to terminate in the case of eager Markov chains. We show that eager Markov chains include those induced by Probabilistic Vector Addition Systems with States, Noisy Turing Machines, and Probabilistic Lossy Channel Systems.
|
|
