互模拟准局部验证算法的扩展与实现

互模拟是并发系统的分析和验证的一个重要概念。本文主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统。我们用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法。我们以VLTS为实验数据基准,进行大量的实验,发现在大多数情况下,前者的性能比后者更好。同时,我们修改了算法使其能够验证模拟关系。最后,我们用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系。     

Bisimilarity for the Region Calculus

A region calculus is a programming language calculus with explicit instrumentation for memory management. Every value is annotated with a region in which it is stored and regions are allocated and deallocated in a stack-like fashion. The annotations can be statically inferred by a type and effect system, making a region calculus suitable as an intermediate language for a compiler of statically typed programming languages.Although a lot of attention has been paid to type soundness properties of different flavors of region calculi, it seems that little effort has been made to develop a semantic framework. In this paper, we present a theory based on bisimulation, which serves as a coinductive proof principle for showing equivalences of polymorphically region-annotated terms. Our notion of bisimilarity is reminiscent of open bisimilarity for the -calculus and we prove it sound and complete with respect to Morris-style contextual equivalence.As an application, we formulate a syntactic equational theory, which is used elsewhere to prove the soundness of a specializer based on region inference. We use our bisimulation framework to show that the equational theory is sound with respect to contextual equivalence.     

LTS中的弱不变量与限制乘积

本文在文献[1,2]的框架下给出了弱不变量的定义,讨论了其性质及与不变量之间的关系。此外,本文还引入了迁移系统的限制乘积概念,并以此为工具研究了弱互模拟和弱不变量之间的相互转化。     

嵌套谓词等式系与弱互模拟

带赋值符号迁移图是一般传值进程的语义模型,其强互模拟等价可以归结为谓词等式系的最大解.该文将这一结果推广到弱互模拟等价,为此,引入嵌套谓词等式系的概念,并提出算法,将带赋值符号迁移图的弱互模拟等价归结为形如E₂μE₁的嵌套谓词等式系的最大解.     

Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Π^p₂-hard. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP.Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a Π^p₂-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and co-NP-hardness.In each of the bisimulation/regularity problems we consider also the classes of normed processes.Note: full version of the paper appears as [18].     

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP have been demonstrated by Stribrna. Mayr achieved recently a result, saying that weak bisimilarity for BPP is Π^p₂-hard. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP.Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a Π^p₂-hardness result by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and co-NP-hardness.In each of the bisimulation/regularity problems we consider also the classes of normed processes.Note: full version of the paper appears as [18].     

Undecidability in the Imitation Game

This paper considers undecidability in the imitation game, the so-called Turing Test. In the Turing Test, a human, a machine, and an interrogator are the players of the game. In our model of the Turing Test, the machine and the interrogator are formalized as Turing machines, allowing us to derive several impossibility results concerning the capabilities of the interrogator. The key issue is that the validity of the Turing test is not attributed to the capability of human or machine, but rather to the capability of the interrogator. In particular, it is shown that no Turing machine can be a perfect interrogator. We also discuss meta-imitation game and imitation game with analog interfaces where both the imitator and the interrogator are mimicked by continuous dynamical systems.     

Bisimilarity enforcing supervisory control for deterministic specifications

This paper studies the supervisory control of nondeterministic discrete event systems to achieve a bisimulation equivalence between the controlled system and the deterministic specification. In particular, a necessary and sufficient condition is given for the existence of a bisimilarity enforcing supervisor, and a polynomial algorithm is developed to verify such a condition. When the existence condition holds, a bisimilarity enforcing supervisor is constructed. Otherwise, two methods are provided for synthesizing supremal feasible sub-specifications.     

An Undecidable Problem for Timed Automata

The reachability problem for timed automata is decidable when the coefficients in the guards are rational numbers. We show that the reachability problem is undecidable when the coefficients are chosen from the set . A consequence of this is that the parameter synthesis problem for timed automata with even a single parameter is undecidable. We discuss why such undecidability results arise in timed and hybrid systems, what they mean, and if it is possible to get around them.     

Undecidability in decentralized supervision

It is well known that supervisor synthesis problems involving partial observations generally have high computational complexity, but was only recently shown (in the preliminary version of this article) that the solvability of decentralized supervisor synthesis problems may be undecidable, even in cases where all pertinent languages are represented as finite automata. The result is established by reduction from the halting problem for Turing machines. Alternative proofs, discovered independently by other authors, employ a reduction from Post's correspondence problem.     

Using Forward Reachability Analysis for Verification of Lossy Channel Systems

We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for computing (i) inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop. All these operations are rather simple and can be carried out in polynomial time.With these techniques, one can straightforwardly construct an algorithm which explores the set of reachable states of a protocol, in order to check various safety properties. We also show how one can perform model-checking of LTL properties, using a standard automata-theoretic construction. It should be noted that all these methods are by necessity incomplete, even for the class of protocols with lossy channels.To illustrate the applicability of our methods, we have developed a tool prototype and used the tool for automatic verification of (a parameterized version of) the Bounded Retransmission Protocol.     

On Symbolic Verification of Weakly Extended PAD

We consider the verification problem of a class of infinite-state systems called wPAD. These systems can be used to model programs with (possibly recursive) procedure calls and dynamic creation of parallel processes. They correspond to PAD models extended with an acyclic finite-state control unit, where PAD models can be seen as combinations of prefix rewrite systems (pushdown systems) with context-free multiset rewrite systems (synchronization-free Petri nets). Recently, we have presented symbolic reachability techniques for the class of PAD based on the use of a class of unranked tree automata. In this paper, we generalize our previous work to the class wPAD which is strictly larger than PAD. This generalization brings a positive answer to an open question on decidability of the model checking problem for wPAD against EF logic. Moreover, we show how symbolic reachability analysis of wPAD can be used in (under) approximate analysis of Synchronized PAD, a (Turing) powerful model for multithreaded programs (with unrestricted synchronization between parallel processes). This leads to a pragmatic approach for detecting the presence of erroneous behaviors in these models based on the bounded reachability paradigm where the notion of bound considered here is the number of synchronization actions.     

Undecidability in Some Structures Related to Computation Theory

We show that many of the so called discrete weak semilatticesconsidered earlier in a series of author's publications havehereditary undecidable first-order theories. Since such structuresappear naturally in some parts of computation theory, we obtainseveral new undecidability results. This applies e.g. to thestructures of complete numberings, of m-degrees of index setsand of the Wadge degrees of k-partitions in the Baire spaceand -algebraic domains. Whenever possible, we try to determinealso the exact degrees of undecidability of the theories underdiscussion.     

Checking Simple Properties of Transition Systems Defined by Thue Specifications

In (possibly infinite) deterministic labeled transition systems defined by Thue congruences, labels are considered as functions of states into states. This paper provides a method for computing domains of such functions for a large class of transition systems. The latter are related to model checking of transition systems defined by Thue congruences.     

A hierarchy of probabilistic system types

We arrange various types of probabilistic transition systems studied in the literature in an expressiveness hierarchy. The expressiveness criterion is the existence of an embedding of systems of the one class into those of the other. An embedding here is a system transformation which preserves and reflects bisimilarity. To facilitate the task, we define the classes of systems and the corresponding notion of bisimilarity coalgebraically and use the new technical result that an embedding arises from a natural transformation with injective components between the two coalgebra functors under consideration. Moreover, we argue that coalgebraic bisimilarity, on which we base our results, coincides with the concrete notions proposed in the literature for the different system classes, exemplified by a detailed proof for the case of general Segala-type systems.     

Bisimilarity control of partially observed nondeterministic discrete event systems and a test algorithm

In this paper, the bisimilarity control of discrete event systems (DESs) under partial observations is investigated, where the plant and the specification are allowed to be nondeterministic. A notation of simulation-based controllability and a synchronization scheme for the supervised system are formalized based on the simulation relation between the specification and the plant. It is shown that the existence of bisimilarity supervisors is characterized by the notions of the simulation-based controllability and the language observability, which extends the traditional results of supervisory control from language equivalence to bisimulation equivalence. In addition, a polynomial algorithm to test the simulation-based controllability is developed by constructing a computing tree. This algorithm together with the test of language observability can be used to check the existence of bisimilarity supervisors.     

Decidability of mean value calculus

Mean Value Calculus(MVC)^[1] is a real-time logic which can be used to specify and verify real-time systems^[2].As a conservative extension of Duration Calculus(DC)^[3],MVC increases the expressive power but keeps the properties of DC.In this paper we present decidability results of MVC.An interesting result is that propositional MVC with chop star operator is still decidable,which develops the results of [4]and [5].     

A semantic framework for open processes

We propose a general methodology for analysing the behaviour of open systems modelled as coordinators, i.e., open terms of suitable process calculi. A coordinator is understood as a process with holes or placeholders where other coordinators and components (i.e., closed terms) can be plugged in, thus influencing its behaviour. The operational semantics of coordinators is given by means of a symbolic transition system, where states are coordinators and transitions are labeled by spatial/modal formulae expressing the potential interaction that plugged components may enable. Behavioural equivalences for coordinators, like strong and weak bisimilarities, can be straightforwardly defined over such a transition system. Different from other approaches based on universal closures, i.e., where two coordinators are considered equivalent when all their closed instances are equivalent, our semantics preserves the openness of the system during its evolution, thus allowing dynamic instantiation to be accounted for in the semantics. To further support the adequacy of the construction, we show that our symbolic equivalences provide correct approximations of their universally closed counterparts, coinciding with them over closed components. For process calculi in suitable formats, we show how tractable symbolic semantics can be defined constructively using unification.