We investigate the synthesis problem for ENCL-systems, defined as Elementary Net Systems extended with context (inhibitor and activator) arcs and explicit event localities. Since colocated events are meant to be executed synchronously, the behaviour of such systems is captured by step transition systems, where arcs are labelled by sets of events rather than by single events. We completely characterise transition systems generated by ENCL-systems after extending the standard notion of a region - defined as a certain set of states - with explicit information about events which, in particular, are responsible for crossing its border. As a result, we are able to construct, for each such transition system, a suitable ENCL-system generating it.
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
The fairness hierarchy and conspiracies, the notions introduced by Best, are studied in the context of elementary nets. Proving that sequential as well as persistent systems are conspiracy-free, we indicate two main roots of conspiracies: distributed memory and conflicts. Using the notion of marking-fairness, due to Merceron, we prove that T0-fairness + M0-fairness = T∞-fairness. This result gives a method of a local control ensuring globally fair executions. Next we show how to check, if a given elementary net is conspiracy-free, and prove the obtained criterion to be effectively decidable. Finally, we give a characterization of live concurrent systems, using the notion of ∞ -fairness.
3
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Bounded Model Checking (BMC) has been recently introduced as an efficient verification method for reactive systems. BMC based on SAT methods consists in searching for a counterexample of a particular length and generating a propositional formula that is satisfiable iff such a counterexample exists. This new technique has been introduced by E. Clarke et al. for model checking of linear time temporal logic (LTL). Our paper shows how the concept of bounded model checking can be extended to ACTL (the universal fragment of CTL). The implementation of the algorithm for Elementary Net Systems is described together with the experimental results.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.