Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

2 Schmidt K.

Powiadomienia systemowe

Sesja wygasła!

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: computer aided verification

Sortuj według:

Ogranicz wyniki do:

Narrowing Petri Net State Spaces Using the State Equation

Schmidt K.

Fundamenta Informaticae

2001

Vol. 47, nr 3,4

325-335

Given a (possibly partially defined) state, all count vectors of transition sequences reaching that state are solutions to a corresponding Petri net state equation. We propose a search strategy where sequences corresponding to a minimal solution of the state equation are explored first. Then step by step the search space is relaxed to arbitrary count vectors. This heuristics relies on the observation that in many (though provably not in all) cases, minimal solutions of the state equation can be realized as a firing sequence. If no target state is reachable, either the state equation does not have solutions, or our search method would yield the full state space. We study the impact of the state equation on reachability, present an algorithm that exploits information from the state equation and discuss its application in stateless search as well as its combination with stubborn set reduction.

Stubborn sets for model checking the EF/AG fragment of CTL

Schmidt K.

Fundamenta Informaticae

2000

Vol. 43, Nr 1-4

331-341

The general stubborn set approach to CTL model checking has the drawback that one either finds a stubborn set with only one enabled transition or one has to expand all enabled transitions. This restriction does not apply in our approach to a fragment of CTL. Furthermore, our reduction does not depend on the invisibility of transitions in a stubborn set.