Tampere University of Technology

TUTCRIS Research Portal

Stubborn sets with frozen actions

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Details

Original languageEnglish
Title of host publicationReachability Problems - 11th International Workshop, RP 2017, Proceedings
PublisherSpringer Verlag
Pages160-175
Number of pages16
ISBN (Print)9783319670881
DOIs
Publication statusPublished - 2017
Publication typeA4 Article in a conference publication
EventINTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS -
Duration: 1 Jan 1900 → …

Publication series

NameLecture Notes in Computer Science
Volume10506
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceINTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS
Period1/01/00 → …

Abstract

Most ample, persistent, and stubborn set methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct all states of the full parallel composition. This problem is solved in this study by a method that is based on “freezing” the actions in the cycle.

Keywords

  • Ignoring problem, Partial-order methods, Safety properties, Stubborn sets

Publication forum classification

Field of science, Statistics Finland