Transition system specifications with negative premises Export

@article{citeulike:4375676, abstract = {In this article the general approach to Plotkin-style operational semantics of Groote and Vaandrager (1989) is extended to transition system specifications (TSSs) with rules that may contain negative premises. Two problems arise: firstly the rules may be inconsistent, and secondly it is not obvious how a TSS determines a transition relation. We present a general method, based on the stratification technique in logic programming, to prove consistency of a set of rules and we show how a specific transition relation can be associated with a TSS in a natural way. Then a special format for the rules, the ntyft/ntyxt format, is defined. It is shown that for this format three important theorems hold. The first theorem says that bisimulation is a congruence if all operators are defined using this format. The second theorem states that, under certain restrictions, a TSS in ntyft format can be added conservatively to a TSS in pure ntyft/ntyxt format. Finally, it is shown that the trace congruence for image-finite processes induced by the pure ntyft/ntyxt format is precisely bisimulation equivalence.}, author = {Groote, J.}, citeulike-article-id = {4375676}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/0304-3975(93)90111-6}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/0304-3975(93)90111-6}, day = {27}, doi = {10.1016/0304-3975(93)90111-6}, issn = {03043975}, journal = {Theoretical Computer Science}, keywords = {concurrency, operationalsemantics}, month = {September}, number = {2}, pages = {263--299}, posted-at = {2009-04-22 16:08:08}, priority = {2}, title = {Transition system specifications with negative premises}, url = {http://dx.doi.org/10.1016/0304-3975(93)90111-6}, volume = {118}, year = {1993} }

TY - JOUR ID - citeulike:4375676 L3 - citeulike-article-id:4375676 N2 - In this article the general approach to Plotkin-style operational semantics of Groote and Vaandrager (1989) is extended to transition system specifications (TSSs) with rules that may contain negative premises. Two problems arise: firstly the rules may be inconsistent, and secondly it is not obvious how a TSS determines a transition relation. We present a general method, based on the stratification technique in logic programming, to prove consistency of a set of rules and we show how a specific transition relation can be associated with a TSS in a natural way. Then a special format for the rules, the ntyft/ntyxt format, is defined. It is shown that for this format three important theorems hold. The first theorem says that bisimulation is a congruence if all operators are defined using this format. The second theorem states that, under certain restrictions, a TSS in ntyft format can be added conservatively to a TSS in pure ntyft/ntyxt format. Finally, it is shown that the trace congruence for image-finite processes induced by the pure ntyft/ntyxt format is precisely bisimulation equivalence. IS - 2 JF - Theoretical Computer Science SN - 03043975 EP - 299 TI - Transition system specifications with negative premises VL - 118 SP - 263 KW - concurrency KW - operationalsemantics AU - Groote, J PY - 1993/09/27/ UR - http://dx.doi.org/10.1016/0304-3975(93)90111-6 ER -