the proceedings contain 27 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Secrecy types for asymmetric communication;type isomorphism...
ISBN:
(纸本)3540418644
the proceedings contain 27 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: Secrecy types for asymmetric communication;type isomorphisms and proof reuse in dependent type theory;on the duality between observability and reachability;the finite graph problem for two-way alternating automata;high-level Petri nets as type theories in the join calculus;temporary data in shared dataspace coordination languages;the complexity of model checking mobile ambients;synchronized tree languages revisited and new applications;computational completeness of programming languages based on graph transformation;class analysis of object-oriented programs through abstract interpretation;foundations for a graph-based approach to the specification of access control policies;categories of processes enriched in final coalgebras;on regular message sequence chart languages and relationships to mazurkiewicz trace theory;decidability of weak bisimilarity for a subset of basic parallel processes;an axiomatic semantics for the synchronous language gentzen and MARRELLA and the verification of an embedded system.
the proceedings contain 36 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: theories for the global ubiquitous computer;choice in dynam...
ISBN:
(纸本)3540212981
the proceedings contain 36 papers. the special focus in this conference is on foundations of softwarescience and computationstructures. the topics include: theories for the global ubiquitous computer;choice in dynamic linking;a language for polynomial time computation;on the existence of an effective and complete inference system for cryptographic protocols;hypergraphs and degrees of parallelism;election and local computations on edges;decidability of freshness, undecidability of revelation;LTL over integer periodicity constraints;unifying recursive and co-recursive definitions in sheaf categories;deriving bisimulation congruences in the DPO approach to graph rewriting;a denotational account of untyped normalization by evaluation;on finite alphabets and infinite bases;specifying and verifying partial order properties using template MSCs;angelic semantics of fine-grained concurrency;on the expressiveness of infinite behavior and name scoping in process calculi;a language for controlling mobile code;distance desert automata and the star height one problem;adhesive categories;a game semantics of local names and good variables;partial correctness assertions provable in dynamic logics;polynomials for proving termination of context-sensitive rewriting;on recognizable timed languages;tree transducers and tree compressions;on term rewriting systems having a rational derivation;duality for labelled markov processes;electoral systems in ambient calculi;canonical models for computational effects;reasoning about dynamic policies;probabilistic bisimulation and equivalence for security analysis of network protocols and strong bisimulation for the explicit fusion calculus.
Transition probabilities are proposed as the stochastic counterparts to set-based relations. We propose the construction of the converse of a stochastic relation. It is shown that two of the most useful properties car...
详细信息
Transition probabilities are proposed as the stochastic counterparts to set-based relations. We propose the construction of the converse of a stochastic relation. It is shown that two of the most useful properties carry over: the converse is idempotent as well as anticommutative. the nondeterminism inherent in a stochastic relation is defined and briefly investigated. We define a bisimulation relation, and indicate conditions under which this relation is transitive;moreover it is shown that bisimulation and converse are compatible. (C) 2004 Elsevier Inc. All rights reserved.
Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper ...
详细信息
ISBN:
(数字)9783540319825
ISBN:
(纸本)3540253882
Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.
A timed extension of pi-calculus with a transaction construct - the calculus Web pi - is studied. the underlying model of Web pi relies on networks of processes;time proceeds asynchronously at the network level, while...
详细信息
ISBN:
(数字)9783540319825
ISBN:
(纸本)3540253882
A timed extension of pi-calculus with a transaction construct - the calculus Web pi - is studied. the underlying model of Web pi relies on networks of processes;time proceeds asynchronously at the network level, while it is constrained by the local urgency at the process level. Namely process reductions cannot be delayed to favour idle steps. the extensional model - the timed bisimilarity - copes with time and asynchrony in a different way with respect to previous proposals. In particular, the discriminating power of timed bisimilarity is weaker when local urgency is dropped. A labelled characterization of timed bisimilarity is also discussed.
the proceedings contain 32 papers from the foundations of softwarescience and computational structures, - 8thinternationalconference, FOSSACS 2005, held as part of the Joint European conferences on theory and Pract...
详细信息
the proceedings contain 32 papers from the foundations of softwarescience and computational structures, - 8thinternationalconference, FOSSACS 2005, held as part of the Joint European conferences on theory and Practices of software, ETAPS 2005, Proceedings. the topics discussed include: mathematical models of computational and combinatorial structures;probabilistic congruence for semistochastic generative processes;stochastic transition systems for continuous state spaces and non-determination;optimal conditional reachability fo multi-priced timed automata;and component refinement and CSC solving for STG decomposition.
the traditional theory of "part of" relations (i.e. mereology) is enriched by adding the formal concept of equivalent and exchangeable parts. Various possible axioms and their roles are discussed. An approac...
详细信息
ISBN:
(纸本)3540287027
the traditional theory of "part of" relations (i.e. mereology) is enriched by adding the formal concept of equivalent and exchangeable parts. Various possible axioms and their roles are discussed. An approach is focused on application to model softwarestructures.
We study the concept of choice for true concurrency models such as prime event structures and safe Petri nets. We propose a dynamic variation of the notion of cluster previously introduced for nets. this new object is...
详细信息
ISBN:
(数字)9783540319825
ISBN:
(纸本)3540253882
We study the concept of choice for true concurrency models such as prime event structures and safe Petri nets. We propose a dynamic variation of the notion of cluster previously introduced for nets. this new object is defined for event structures, it is called a branching cell. Our aim is to bring an interpretation of branching cells as a right notion of "local state", for concurrent systems. We illustrate the above claim through applications to probabilistic concurrent models. In this respect, our results extends in part previous work by Varacca-Volzer-Winskel on probabilistic confusion free event structures. We propose a construction for probabilities over so-called locally finite event structuresthat makes concurrent processes probabilistically independent-simply attach a dice to each branching cell;dices attached to concurrent branching cells are thrown independently. Furthermore, we provide a true concurrency generalization of Markov chains, called Markov nets. Unlike in existing variants of stochastic Petri nets, our approach randomizes Mazurkiewicz traces, not firing sequences. We show in this context the Law of Large Numbers (LLN), which confirms that branching cells deserve the status of local state. Our study was motivated by the stochastic modeling of fault propagation and alarm correlation in telecommunications networks and services. It provides the foundations for probabilistic diagnosis, as well as the statistical distributed learning of such models.
Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this pa...
详细信息
Groupoidal relative pushouts (GRPOs) have recently been proposed by the authors as a new foundation for Leifer and Milner's approach to deriving labelled bisimulation congruences from reduction systems. In this paper, we develop the theory of GRPOs further, proving that well-known equivalences, other than bisimulation, are congruences. To demonstrate the type of category theoretic arguments which are inherent in the 2-categorical approach, we construct GRPOs in a category of 'bunches and wirings.' Finally, we prove that the 2-categorical theory of GRPOs is a generalisation of the approaches based on Milner's precategories and Leifer's functorial reactive systems. (c) 2004 Elsevier B.V. All rights reserved.
暂无评论