Transition system specifications with negative premises
The general approach to Plotkin style operational semantics of \textit{J. F. Groote} and \textit{F. W. Vaandrager} [Structured operational semantics and bisimulation as a congruence, Inf. Comput. 100, No. 2, 202-260 (1992; Zbl 0752.68053)] is extended to Transition System Specifications (TSS's) with rules that may contain negative premises. Two problems arise: firstly the rules may be inconsistent, and secondly it is not obvious how a consistent TSS should determine 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 format of the rules, called the ntyft/ntyxt-format, is defined. A rule is in ntyft-format if it has the form \[ {\{t_ k\overset {a_ k} \longrightarrow y_ k\mid k\in K\}\cup \{t_ l\overset {b_ l} \nrightarrow \mid l\in L\}}\over f(x_ 1,...,x_ n)\overset {a} \longrightarrow t \] where \(K,L\) are index sets, \(t_ k,t_ i,t\) terms, \(y_ k,x_ 1,...,x_ n\) pairwise different variables, \(f\) a function symbol and \(a_ k,b_ l,a\) transition labels. A rule is in ntyxt-format if it is an instantiation of \[ {\{t_ k\overset {a_ k} \longrightarrow y_ k\mid k\in K\}\cup \{t_ l\overset {b_ l} \nrightarrow \mid l\in L\}}\over x\overset {a} \longrightarrow t \] where \(x\) is a variable, different from \(y_ k\). The ntyft/ntyxt-format is an extension of the tyft/tyxt-format that has been introduced in [loc. cit.]. It is shown that for the ntyft/ntyxt-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.
- A calculus of communicating systems
- Algebraic laws for nondeterminism and concurrency
- Algèbre de processus et synchronisation
- Bisimulation can't be traced
- Bisimulation through probabilistic testing
- Calculi for synchrony and asynchrony
- Global renaming operators in concrete process algebra
- Higher-level synchronising devices in Meije-SCCS
- scientific article; zbMATH DE number 4199656 (Why is no real title available?)
- scientific article; zbMATH DE number 3808928 (Why is no real title available?)
- scientific article; zbMATH DE number 3919813 (Why is no real title available?)
- scientific article; zbMATH DE number 3990852 (Why is no real title available?)
- scientific article; zbMATH DE number 3716792 (Why is no real title available?)
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 176757 (Why is no real title available?)
- scientific article; zbMATH DE number 1142320 (Why is no real title available?)
- scientific article; zbMATH DE number 4001464 (Why is no real title available?)
- Observation equivalence as a testing equivalence
- Structured operational semantics and bisimulation as a congruence
- The Esterel synchronous programming language: Design, semantics, implementation
- Semantics and expressiveness of ordered SOS
- A process algebraic view of Linda coordination primitives
- Structured operational semantics and bisimulation as a congruence
- A conservative look at operational semantics with variable binding
- A general conservative extension theorem in process algebras with inequalities
- An alternative formulation of operational conservativity with binding terms.
- Algebraic theory of probabilistic and nondeterministic processes.
- Comparing three semantics for Linda-like languages
- Finite axiom systems for testing preorder and De Simone process languages
- Language preorder as a precongruence
- The theory of interactive generalized semi-Markov processes
- Process algebra and conditional composition
- Divide and congruence. II: From decomposition of modal formulas to preservation of delay and weak bisimilarity
- Discrete time generative-reactive probabilistic processes with different advancing speeds
- A comparison of Statecharts step semantics
- On the expressiveness of Linda coordination primitives.
- Absolute versus relative time in process algebras.
- Ordered SOS process languages for branching and eager bisimulations
- The meaning of negative premises in transition system specifications. II
- Process languages with discrete relative time based on the ordered SOS format and rooted eager bisimulation
- A format for semantic equivalence comparison
- Rooted branching bisimulation as a congruence
- Probabilistic divide \& congruence: branching bisimilarity
- Ensuring liveness properties of distributed systems: open problems
- Bialgebraic foundations for the operational semantics of string diagrams
- On the axiomatisability of priority. III: Priority strikes again
- Divide and congruence. III: From decomposition of modal formulas to preservation of stability and divergence
- Compositionality of Hennessy-Milner logic by structural operational semantics
- A unified rule format for bounded nondeterminism in SOS with terms as labels
- Reduction semantics in Markovian process algebra
- A process algebraic view of shared dataspace coordination
- Notions of bisimulation and congruence formats for SOS with data
- A general SOS theory for the specification of probabilistic transition systems
- Compositional equivalences based on open pNets
- Reactive bisimulation semantics for a process algebra with timeouts
- Structural operational semantics with first-order logic
- A congruence rule format with universal quantification
- scientific article; zbMATH DE number 7449995 (Why is no real title available?)
- A pre-congruence format for XY-simulation
- Branching vs. Linear Time: Semantical Perspective
- scientific article; zbMATH DE number 176757 (Why is no real title available?)
- Divide and congruence: from decomposition of modal formulas to preservation of branching and -bisimilarity
- Rule formats for determinism and idempotence
- The meaning of negative premises in transition system specifications
- Process algebra with four-valued logic
- scientific article; zbMATH DE number 1479628 (Why is no real title available?)
- Sequent calculi for default and autoepistemic logics
- Tree rules in probabilistic transition system specifications with negative and quantitative premises
- SOS rule formats for convex and abstract probabilistic bisimulations
- scientific article; zbMATH DE number 7559462 (Why is no real title available?)
- Rule formats for nominal process calculi
- Divide and congruence. III: Stability \& divergence
- Some undecidable properties of SOS specifications
- Barbed bisimulation
- On recursive operations over logic LTS
- Axiomatizing maximal progress and discrete time
- Sequencing and intermediate acceptance: Axiomatisation and decidability of bisimilarity
- Bialgebraic semantics for string diagrams
- Pushdown Automata and Context-Free Grammars in Bisimulation Semantics
- Variable binding operators in transition system specifications
- Bochvar-McCarthy logic and process algebra
- Quantales, finite observations and strong bisimulation
- Back to the format: a survey on SOS for probabilistic processes
- Modal and temporal logics for processes
- Structural operational semantics for weak bisimulations
- Parallel pushdown automata and commutative context-free grammars in bisimulation semantics (extended abstract)
- Sequential value passing yields a Kleene theorem for processes
- Rooted branching bisimulation as a congruence for probabilistic transition systems
- A syntactic commutativity format for SOS
- SOS formats and meta-theory: 20 years after
- A precongruence format for should testing preorder
This page was built for publication: Transition system specifications with negative premises
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685387)
