Vector addition systems (VAS) constitute an important model of computation and concurrency that is equally expressive as the Petri net model. Recently, a lot of research has been conducted on vector addition systems with states (VASS), which are VASes equipped with a finite state control. Results on VASS naturally carry over to VAS, but no straightforward improvement is available. In this paper, we investigate the reachability problem in VAS in fixed dimensions. Based on a pumpability analysis of VAS that refines Rackoff’s extraction for VASS, we obtain an F_{d-2} upper bound for the d-dimensional VAS reachability problem, improving the F_d upper bound inherited from the d-dimensional VASS reachability problem. Low-dimensional VASes are also considered. In particular, we establish a PSPACE upper bound for reachability in 4-dimensional VAS and an ELEMENTARY upper bound for 5-dimensional VAS, while the same upper bounds were known only for 2-VASS and 3-VASS, respectively. The result for 4-VAS particularly hinges on a simplified projection technique developed for geometrically 2-dimensional VASSes, whose reachability problem is shown to be equivalent to 2-VASS.

Recently a divergence-sensitive branching bisimilarity has been proposed and studied for the randomized CCS model. In this article, we give an equivalent inductive characterization for the bisimilarity, which is a probabilistic extension of the previous work on the non-probabilistic model. Based on the new characterization, a novel polynomial-time verification algorithm for the divergence-sensitive branching bisimilarity is proposed.

An $\mathsf{F}_{d}$ upper bound for the reachability problem in vector addition systems with states (VASS) in fixed dimension is given, where $\mathsf{F}_d$ is the $d$-th level of the Grzegorczyk hierarchy of complexity classes. The new algorithm combines the idea of the linear path scheme characterization of the reachability in the $2$-dimension VASSes with the general decomposition algorithm by Mayr, Kosaraju and Lambert. The result improves the $\mathsf{F}_{d + 4}$ upper bound due to Leroux and Schmitz (LICS 2019).

Abstract Petri nets form a concurrent model for distributed and asynchronous systems. They are capable of modeling information flow in a closed system, but are generally not suitable for the study of compositionality. We address the issue of Petri net compositionality by introducing extensional Petri nets. In an extensional Petri net some places are external while others are internal. Every external place is labeled by a distinguished interface name. When composing two extensional Petri nets two places with a same label are coerced. An external place can be turned into an internal place by applying localization operator. The paper takes a look at bisimulation semantics and observational properties of the extensional Petri nets.

It is shown that generally higher order process calculi cannot be interpreted in name-passing calculi in a robust way.

Divergence and non-determinism play a fundamental role in the theory of computation, and their combined effect on computational equality deserves further study. By looking at the issue from the point of view of both computation and interaction, we are led to a canonical equality for non-deterministic computation, revealing its rich algebraic structure. We study this structure in three ways. First, we construct a complete equational system for finite-state non-deterministic computation. The challenge with such a system is to find an equational alternative to fixpoint inductionà laMilner. We establish a negative result in the form of the non-existence of a finite equational system for the canonical equality of non-deterministic computation to support our approach. We then investigate infinite-state non-deterministic computation in the light of definability and show that every recursively enumerable set is generated by an unobservable process. Finally, we prove that, as far as computation is concerned, the effect produced jointly by divergence and non-determinism is model independent for a large class of process models. We use C-graphs, which are interesting in their own right, as abstract representations of the computational objects throughout the paper.

This special issue contains selected papers from the Eighth Asian Symposium on Programming Languages and Systems (APLAS 2010), held from 28 November – 1 December 2010, in Shanghai, China. The symposium was sponsored by the Asian Association for Foundation of Software (AAFS) and Shanghai Jiao Tong University.

A general approach is proposed for transforming objects to methods on the fly in the framework of the π-calculus. The power of the approach is demonstrated by applying it to generate an encoding of the full lambda calculus in the π-calculus. The encoding is proved to preserve and reflect beta reduction, and is shown to be fully abstract with respect to Abramsky's applicative bisimilarity.

In this paper a systematic study of bisimilarities on asymmetric chine-processes is carried out. The notion of L-bisimilarities on asymmetric chine-processes is introduced. Twelve distinct L-bisimilarities are derived from all of L-bisimilarities by constructing a bisimulation lattice. For each of these twelve distinct L-bisimilarities, its open version is defined and showed to coincide with it, and then its congruence is presented. Three update laws are proposed and three tau laws are modified. Finally, sound complete equational systems are established for twelve congruences

The analysis of stability and robustness of fuzzy reasoning is an important issue in areas like intelligent systems and fuzzy control. An interesting aspect is to what extent the perturbation of input in a fuzzy reasoning scheme causes the oscillation of the output. In particular, when the error limits (restrictions) of the input values are given, what the error limits of the output values are. In this correspondence, we estimate the upper and lower bounds of the output error affected by the perturbation parameters of the input, and obtain the limits of the output values when the input values range over some interval in many fuzzy reasoning schemes under compositional rule of fuzzy inference (CRI).

The spi calculus has been proved useful for reasoning about security protocols. It is however difficult to mechanize the equivalence checking in that framework due to the complexity caused by name passing communications. The paper proposes a calculus for the analysis of the security protocols (SPC for short) as a simplification of the spi calculus. SPC can explicitly express environment knowledge, protocol participants and their knowledge. We present its syntax and semantics, and specify some security properties in terms of equivalence relations. Finally two examples of formal verification is given.

Abstract. A schematic law dealing with localization operator is proposed for pi calculus. It is shown that the law renders the use of distinction unnecessary in the axiomatic theory of open congruence. 1

In this paper we define a logical framework, called &;lambda;TT, that is well suited for semantic analysis. We introduce the notion of a fibration [Lscr ]1 : [Fscr ]1 [xrarr ] [Cscr ] 1 being internally definableThe definability as used in this paper should not be confused with Bénabou's ‘definability’ (Bénabou 1985). in a fibration [Lscr ]2 : [Fscr ]2 [xrarr ] [Cscr ] 2. This notion amounts to distinguishing an internal category L in [Lscr ]2 and relating [Lscr ]1 to the externalization of L through a pullback. When both [Lscr ]1 and [Lscr ]2 are term models of typed calculi [Lscr ]1 and [Lscr ]2, respectively, we say that [Lscr ]1 is an internal typed calculus definable in the frame language [Lscr ]2. We will show by examples that if an object language is adequately represented in λTT, then it is an internal typed calculus definable in the frame language λTT. These examples also show a general phenomenon: if the term model of an object language has categorical structure S, then an adequate encoding of the language in λTT imposes an explicit internal categorical structure S in the term model of λTT and the two structures are related via internal definability. Our categorical investigation of logical frameworks indicates a sensible model theory of encodings.

We give an interpretation of Martin-Löf's type theory (with universes) extended with generalized inductive types. The model is an extension of the recursive model given by Beeson. By restricting our attention to PER model, we show that the strictness of positivity condition in the definition of generalized inductive types can be dropped. It therefore gives an interpretation of general inductive types in Martin-Löf's type theory.