1,721,077 research outputs found
An Axiomatic Semantics for the Synchronous Language Gentzen
No full textAbstractWe propose an axiomatic semantics for the synchronous language Gentzen, which is an instantiation of the paradigm Timed Concurrent Constraint Programming proposed by Saraswat, Jagadeesan and Gupta. We view Gentzen as a prototype of the class of state-oriented synchronous languages, since it offers the basic constructs that are shared by the languages in the class. Since synchronous concurrency cannot be simulated by arbitrary interleaving, we cannot exploit “head normal forms”, on which axiomatic theories for asynchronous process calculi are based. We suggest how axiomatic semantics for other state-oriented synchronous languages can be obtained by expressing constructs of such languages in terms of Gentzen constructs
Timed CCP Compositionally Embeds Argos and Lustre
No full textWe prove that both the synchronous data-flow language Lustre restricted to types with finite values and the synchronous state-oriented language Argos are embedded in the synchronous paradigm Timed Concurrent Constraint Programming (tccp). In fact, for each of the two languages we provide a tccp language encoding it compositionally with respect to the syntax of programs and linearly with respect to the size of programs. Besides giving results of expressiveness for tccp, our encodings permit us to obtain a language tailored for programming reactive systems where both control handling aspects and data processing aspects are relevant
Rule Formats for Compositional Non Interference Properties
No full textWe introduce the transition rule formats rooted SBSNNI and CP_BNDC. We prove that the non-interference property rooted SBSNNI introduced in the present paper, and the already known non-interference property CP_BNDC, are preserved by constructs of all process algebras with SOS transition rules respecting the restrictions of the formats rooted SBSNNI and CP_BNDC, respectively. To show that our formats have practical applications, we prove that a slight variant of Focardi and Gorrieri's Security Process Algebra, the Kleene star recursion construct, the replication construct of polyadic π-calculus, and a process algebra extending BPAετ to deal with two level systems, respect both formats. By means of some counterexamples, we prove also that all restrictions of the formats are necessary
An Axiomatic Semantics for Esterel
No full textAbstractIn this paper we propose an axiomatic semantics for the synchronous language Esterel. We begin with giving a structural operational semantics for Esterel in terms of a labeled transition system (LTS). We prove that bisimulation on LTS states (which correspond to Esterel programs) is a congruence and that our LTS reflects the input/output behavior of programs. So, bisimilar programs are distinguished neither by any Esterel context nor by the external environment, and bisimulation is a reasonable notion of behavioral equivalence. In order to characterize equivalent programs, we give a set of axioms and we prove that they induce an axiomatization over Esterel which is sound and complete modulo bisimulation
Notes on Generative Probabilistic Bisimulation
No full textAbstractIn this notes we consider the model of Generative Probabilistic Transition Systems, and Baier and Hermanns' notion of weak bisimulation defined over them. We prove that, if we consider any process algebra giving rise to a Probabilistic Transition System satisfying the condition of regularity and offering prefixing, interleaving, and guarded recursion, then the coarsest congruence that is contained in weak bisimulation is strong bisimulation
- …
