| 1. |
|
|
| 2. |
- 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)
|
|
| 3. |
- Abdulla, Parosh, et al.
(författare)
-
A Survey of Regular Model Checking.
- 2004
-
Ingår i: CONCUR 2004 - Concurrency Theory. - 354022940X ; , s. 35-48
-
Konferensbidrag (refereegranskat)abstract
- Regular model checking is being developed for algorithmic verification of several classes of infinite-state systems whose configurations can be modeled as words over a finite alphabet. Examples include parameterized systems consisting of an arbitrary number of homogeneous finite-state processes connected in a linear or ring-formed topology, and systems that operate on queues, stacks, integers, and other linear data structures. The main idea is to use regular languages as the representation of sets of configurations, and finite-state transducers to describe transition relations. In general, the verification problems considered are all undecidable, so the work has consisted in developing semi-algorithms, and decidability results for restricted cases. This paper provides a survey of the work that has been performed so far, and some of its applications.
|
|
| 4. |
- Abdulla, Parosh, et al.
(författare)
-
Regular Model Checking for LTL(MSO)
- 2004
-
Ingår i: Computer Aided Verification. - 3540223428 ; , s. 348-360
-
Konferensbidrag (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present $\logic$, a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. $\logic$ is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process.We give a technique for model checking $\logic$, which is adapted from the automata-theoretic approach: a formula is translated to a (\buchi) transducer with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique and show its application to a number of parameterized algorithms from the literature.
|
|
| 5. |
- Abdulla, Parosh, et al.
(författare)
-
Regular model checking for LTL(MSO)
- 2012
-
Ingår i: International Journal on Software Tools for Technology Transfer. - Springer : Springer Science and Business Media LLC. - 1433-2779 .- 1433-2787. ; 14:2, s. 223-241
-
Tidskriftsartikel (refereegranskat)abstract
- Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of states. We present LTL(MSO), a combination of the logics MSO and LTL as a natural logic for expressing temporal properties to be verified in regular model checking. In other words, LTL(MSO) is a natural specification language for both the system and the property under consideration. LTL(MSO) is a two-dimensional modal logic, where MSO is used for specifying properties of system states and transitions, and LTL is used for specifying temporal properties. In addition, the first-order quantification in MSO can be used to express properties parameterized on a position or process. We give a technique for model checking LTL(MSO), which is adapted from the automata-theoretic approach: a formula is translated to a Buechi regular transition system with a regular set of accepting states, and regular model checking techniques are used to search for models. We have implemented the technique, and show its application to a number of parameterized algorithms from the literature.
|
|
| 6. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2005
-
Ingår i: Electr. Notes on Theoret. Comput. Sci.. ; 118, s. 3-18
-
Tidskriftsartikel (refereegranskat)
|
|
| 7. |
|
|
| 8. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2005
-
Ingår i: Electronical Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661 .- 1571-0661. ; 118, s. 3-18
-
Tidskriftsartikel (refereegranskat)abstract
- Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.
|
|
| 9. |
- Berg, Therese, et al.
(författare)
-
Insights to Angluin's Learning
- 2003
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results.
|
|
| 10. |
|
|
