Academic
Publications
Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties

Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties,Laura Bozzelli

Model Checking for Process Rewrite Systems and a Class of Action-Based Regular Properties   (Citations: 3)
BibTex | RIS | RefWorks Download
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Only recently, Bozzelli [3 ]h as demonstrated that model checking of infinite runs is decidable for PRS and the fragment of LTL capturing exactly fairness properties...
    • ...The proof employs our results presented in [3,9,11] to reduce the problem to LTL model checking for PDA and PN. This result directly implies decidability of the model checking problem for wPRS and negated formulae of A. 2. We show that every formula of the basic fragment LTL(Fs, Gs) (i.e., the fragment with modalities strict eventually and strict always only) can be effectively translated into A. As LTL(Fs, Gs) is closed under negation, we ...
    • ...All conditions of the definition can be checked due to the following lemma, results of [3], and decidability of LTL model checking for PDA and PN. Lemma 3 says that every PRS in normal form can be transformed into an “equivalent” flat system...
    • ...is a special case of the fairness problem, which is decidable due to [3]...
    • ...Such a fairness condition corresponds to an automaton that isnot1-weak.Fortunately,thereisaresultof[3]sayingthattheproblemwhetheraPRShasan infinite run satisfying a given fairness condition is decidable...

    Laura Bozzelliet al. On decidability of LTL model checking for process rewrite systems

    • ...Only recently, we have demonstrated that model checking of innite runs is decidable for PRS and the fragment of LTL capturing exactly fairness properties [Boz05]...
    • ...The proof employs our results presented in [Boz05,K RS04a,K RS05] to reduce the problem to LTL model checking for PDA and PN. Thus we get decidability of model checking for wPRS against LTL . Note that LTL is strictly more expressive than the Lamport logic (i.e...
    • ...All conditions of the denition can be checked due to the following lemma, [Boz05], and decidability of LTL model checking for PDA and PN. Lemma 7 says that every PRS in normal form can be transformed into an ìequivalentî at system...
    • ...B C is a special case of the fairness problem, which is decidable due to [Boz05]...
    • ...So far, only two positive results on LTL model checking of PA (and classes subsuming PA) have been published: decidability of model checking of innite runs for PRS and LTL fragment of fairness properties [Boz05] and decidability of the same problem for PA and simple PLTL [BH96]...
    • ...It is also worth mentioning that our proof techniques differ from those used in [Boz05] and [BH96]...

    Laura Bozzelliet al. On Decidability of LTL Model Checking for Process Rewrite Systems

    • ...Model che cking of infinite runs is decidable for the PA class and the fragment simple PLTL2, see [2], and also for the PRS class and a fragment of LTL expressing exactly fairness properties [3]...

    Mojm ´ iret al. On Decidability of LTL+Past Model Checking for Process Rewrite Systems

Sort by: