We take the point of view that, if transition systems are coalgebras for a functor T, then an adequate logic for these transition systems should arise from the 'Stone dual' L of T. We show that such a functor ...
详细信息
Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to semantic interpolation, we generate, prove and classify a series of interpolation results for first-order l...
详细信息
A key problem in mixing operational (e.g., process-algebraic) and declarative (e.g., logical) styles of specification is how to deal with inconsistencies arising when composing processes under conjunction. this paper ...
详细信息
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 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.
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.
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.
暂无评论