Search

A communicating system is k -synchronizable if all of the message sequence charts representing the executions can be divided into slices of k sends followed by k receptions. It was previously shown that, for a fixed given k , one could decide whether a communicating system is k -synchronizable. This result is interesting because the reachability problem can be solved for k -synchronizable systems. However, the decision procedure assumes that the bound k is fixed. In this paper we improve this result and show, for mailbox communication, that it is possible to decide if such a bound k exists. [ABSTRACT FROM AUTHOR]

ANDy, Activity Networks with Delays, is a discrete framework aiming at the qualitative modeling of time-dependent activities. The modular and expressive syntax makes ANDy suitable for a concise and natural modeling of time-dependent biological systems (i.e., regulatory pathways). Activities involve entities playing the role of activators, inhibitors or products of biochemical network operation. Activities may have a given duration, i.e., the time required to obtain results. An entity may represent an object (e.g., an agent, a biochemical species or a family of thereof) with a local attribute, a state denoting its level (e.g., concentration, strength). Entity levels may change as a result of an activity or may decay gradually as time passes by. The semantics of ANDy is formally given via high-level Petri nets ensuring this way some modularity. As main results we show that ANDy systems have finite state representations even for potentially infinite processes and it well adapts to the modeling of toxic behaviors. As an illustration, we present a classification of toxicity properties and give some hints on how they can be verified on ANDy systems with existing tools. A case study on blood glucose regulation is provided to exemplify the ANDy framework and the toxicity properties. [ABSTRACT FROM AUTHOR]

Session types offer a powerful type-theoretic foundation for the analysis of structured communications, as commonly found in service-oriented systems. They are defined upon core programming calculi which offer only limited support for expressing requirements related to runtime adaptation . This is unfortunate, as service-oriented systems are increasingly being deployed upon highly dynamic infrastructures in which such requirements are central concerns. In previous work, we developed a process calculi framework of adaptable processes , in which concurrent processes can be replaced, suspended, or discarded at runtime. In this paper, we propose a session type discipline for a calculus with adaptable processes. Our typed framework offers a simple alternative for integrating runtime adaptation mechanisms in the modeling and analysis of structured communications. We show that well-typed processes enjoy safety and consistency properties: while the former property ensures the absence of communication errors at runtime, the latter guarantees that active session behavior is never disrupted by adaptation actions. [ABSTRACT FROM AUTHOR]

Constraint Handling Rules (CHR) is a committed-choice declarative language that has been originally designed for writing constraint solvers and is nowadays a general purpose language. CHR programs consist of multiheaded guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. Many empirical evidences suggest that multiple heads augment the expressive power of the language, however no formal result in this direction has been proved, so far. In the first part of this article we analyze the Turing completeness of CHR with respect to the underlying constraint theory. We prove that if the constraint theory is powerful enough then restricting to single head rules does not affect the Turing completeness of the language. On the other hand, differently from the case of the multiheaded language, the single head CHR language is not Turing powerful when the underlying signature (for the constraint theory) does not contain function symbols. In the second part we prove that, no matter which constraint theory is considered, under some reasonable assumptions it is not possible to encode the CHR language (with multi-headed rules) into a single headed language while preserving the semantics of the programs. We also show that, under some stronger assumptions, considering an increasing number of atoms in the head of a rule augments the expressive power of the language. These results provide a formal proof for the claim that multiple heads augment the expressive power of the CHR language. [ABSTRACT FROM AUTHOR]