scholarly journals Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components

1997 ◽  
Vol 26 (519) ◽  
Author(s):  
Allan Cheng ◽  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
The State ◽  
Connected Components ◽  
Coloured Petri Nets ◽  
Transition Systems ◽  
Strongly Connected Components ◽  
State Spaces ◽  
Labelled Transition Systems ◽  
Strongly Connected

In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.

scholarly journals On the Power of Labels in Transition Systems

2001 ◽  
Vol 8 (19) ◽  
Author(s):  
Jirí Srba
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Transition Systems ◽  
Labelled Transition Systems ◽  
Pushdown Automata ◽  
General Reduction

In this paper we discuss the role of labels in transition systems with regard to bisimilarity and model checking problems. We suggest a general reduction from labelled transition systems to unlabelled ones, preserving bisimilarity and satisfiability of mu-calculus formulas. We apply the reduction to the class of transition systems generated by Petri nets and pushdown automata, and obtain several decidability/complexity corollaries for unlabelled systems. Probably the most interesting result is undecidability of strong bisimilarity for unlabelled Petri nets.

ENHANCING ADEQUACY OF GRADING STUDY PROJECTS ON THE BASE OF PARAMETRIC RELAXATION OF PAIRWISE COMPARISONS

2021 ◽  
Vol 1 ◽  
pp. 122-133
Author(s):  
Alexey V. Oletsky ◽  
◽  
Mikhail F. Makhno ◽  
◽  
Keyword(s):  
Center Of Mass ◽  
Estimation Algorithm ◽  
Relaxation Parameter ◽  
Connected Components ◽  
Pairwise Comparisons ◽  
Strongly Connected Components ◽  
Standard Scale ◽  
Relaxation Parameters ◽  
Strongly Connected ◽  
The One

A problem of automated assessing of students’ study projects is regarded. A heuristic algorithm based on fuzzy estimating of projects and on pairwise comparisons among them is proposed. For improving adequacy and naturalness of grades, an approach based on introducing a parameter named relaxation parameter was suggested in the paper. This enables to reduce the spread between maximum and minimum values of projects in comparison with the one in the standard scale suggested by T. Saati. Reasonable values of this parameter were selected experimentally. For estimating the best alternative, a center of mass of a fuzzy max-min composition should be calculated. An estimation algorithm for a case of non-transitive preferences based on getting strongly connected components and on pairwise comparisons between them is also suggested. In this case, relaxation parameters should be chosen separately for each subtask. So the combined technique of evaluating alternatives proposed in the paper depends of the following parameters: relaxation parameters for pairwise comparisons matrices within each strongly connected components; relaxation parameter for pairwise comparisons matrices among strongly connected components; membership function for describing the best alternative.

Sign in / Sign up

Export Citation Format

Share Document