| 1. |
- Churchill, Martin, et al.
(författare)
-
Modular Semantics for Transition System Specifications with Negative Premises
- 2013
-
Ingår i: Proceedings of the 24th International Conference on Concurrency Theory. - Heidelberg : Springer Berlin/Heidelberg. - 9783642401831 - 9783642401848 ; , s. 46-60
-
Konferensbidrag (refereegranskat)abstract
- Transition rules with negative premises are needed in the structural operational semantics of programming and specification constructs such as priority and interrupt, as well as in timed extensions of specification languages. The well-known proof-theoretic semantics for transition system specifications involving such rules is based on well-supported proofs for closed transitions. Dealing with open formulae by considering all closed instances is inherently non-modular - proofs are not necessarily preserved by disjoint extensions of the transition system specification. Here, we conservatively extend the notion of well-supported proof to open transition rules. We prove that the resulting semantics is modular, consistent, and closed under instantiation. Our results provide the foundations for modular notions of bisimulation such that equivalence can be proved with reference only to the relevant rules, without appealing to all existing closed instantiations of terms. © 2013 Springer-Verlag.
|
|
| 2. |
- Mosses, Peter D., et al.
(författare)
-
Robustness of Behavioral Equivalence on Open Terms
- 2010
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity on open terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrary sound equations on open terms are preserved by all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of them to be sufficient for preserving ci-bisimilarity.
|
|
