Analysis and modeling of web services flow using π-calculus

In order to increase the effectiveness and the reliability of web services flow, the ~r-calculus formal method is introduced as a development language for web services flow. The π-calculus overcomes inabilities of web service flow languages in demonstrating the consistency, validating the correctness and so on. The π- calculus analysis and modeling of web services flow is presented, the dynamic actions and basic activities of WS-BPEL with π-calculus formally are described, and the mapping from π-calculus expression to WS-BPEL is built. The basic construction of web services flow with the π-calculus method after the analysis of the syntax of WS-BPEL and inter-description between WS-BPEL and π-calculus is expressed. Also discussed are the approaches to web services flow by modeling from different views, and the proposed approaches through the development and modeling of an e-commerce web service flow application are illustrated.

Control of Non-Deterministic Systems With μ-Calculus Specifications Using Quotienting

The supervisory control problem for discrete event system(DES) under control involves identifying the supervisor, if one exists, which, when synchronously composed with the DES,results in a system that conforms to the control specification. In this context, we consider a non-deterministic DES under complete observation and control specification expressed in action-based propositional μ-calculus. The key to our solution is the process of quotienting the control specification against the plan resulting in a new μ-calculus formula such that a model for the formula is the supervisor. Thus the task of control synthesis is reduced a problem of μ-calculus satisfiability. In contrast to the existing μ-calculus quotienting-based techniques that are developed in deterministic setting, our quotienting rules can handle nondeterminism in the plant models. Another distinguishing feature of our technique is that while existing techniques use a separate μ-calculus formula to describe the controllability constraint(that uncontrollable events of plants are never disabled by a supervisor), we absorb this constraint as part of quotienting which allows us to directly capture more general state-dependent controllability constraints. Finally, we develop a tableau-based technique for verifying satisfiability of quotiented formula and model generation. The runtime for the technique is exponential in terms of the size of the plan and the control specification. A better complexity result that is polynomial to plant size and exponential to specification size is obtained when the controllability property is state-independent. A prototype implementation in a tabled logic programming language as well as some experimental results are presented.

δ-Calculus:A New Approach to Quantifying Location Privacy

With the rapid development of mobile wireless Internet and high-precision localization devices,location-based services(LBS)bring more convenience for people over recent years.In LBS,if the original location data are directly provided,serious privacy problems raise.As a response to these problems,a large number of location-privacy protection mechanisms(LPPMs)(including formal LPPMs,FLPPMs,etc.)and their evaluation metrics have been proposed to prevent personal location information from being leakage and quantify privacy leakage.However,existing schemes independently consider FLPPMs and evaluation metrics,without synergizing them into a unifying framework.In this paper,a unified model is proposed to synergize FLPPMs and evaluation metrics.In detail,the probabilistic process calculus(calledδ-calculus)is proposed to characterize obfuscation schemes(which is a LPPM)and integrateα-entropy toδ-calculus to evaluate its privacy leakage.Further,we use two calculus moving and probabilistic choice to model nodes’mobility and compute its probability distribution of nodes’locations,and a renaming function to model privacy leakage.By formally defining the attacker’s ability and extending relative entropy,an evaluation algorithm is proposed to quantify the leakage of location privacy.Finally,a series of examples are designed to demonstrate the efficiency of our proposed approach.

Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem causedby instantiating input names with all names in the standard definition of bisimulation in л-calculus. However, it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly. In this paper a new notionof bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names. It is shownthat the new notion captures symbolic bisimulation in a precise sense. Based on thenew definition an efficient algorithm, which instantiates input names 'on-the-fly', ispresented to check bisimulations for finite-control л-calculus.

Symbolic transition graph and its early bisimulation checking algorithms for the π-calculus

Symbolic transition graph is proposed as an intuitive and compact semantic model for the π-calculus processes.Various versions (strong/weak, ground/symbolic) of early operational semantics are given to such graphs. Based on them the corresponding versions of early bisimulation equivalences and observation congruence are defined. The notions of symbolic observation graph and symbolic congruence graph are also introduced, and followed by two theorems ensuring the elimination of τ-cycles and τ-edges. Finally algorithms for checking strong/weak early bisimulation equivalences and observation congruence are presented together with their correctness proofs. These results fuse and generalize the strong bisimulation checking algorithm for value-passing processes and the verification technique for weak bisimulation of pure-CCS to the finite control π-calculus.

Symmetric π-Calculus

An alternative presentation of the π-calculus is given. This version of the π-calculus is symmetric in the sense that communications are symmetric and there is no dtherence between input and output prehxes. The point of the symmetric π-calculus is that it has no abstract names. The set of closed names is therefore homogeneous. The π-calculus can be fully embedded into the symmtric π-calculus. The symmetry changes the emphasis of the communication mechanism of the π-calculus and opens up possibility for further variations.

A Service-Oriented Architecture of Cyber-Physical System and Study on Two Key Issues

As the basis of designing and implementing a cyber-physical system (CPS), architecture research is very important but still at preliminary stage. Since CPS includes physical components, time and space constraints seriously challenge architecture study. In this paper, a service-oriented architecture of CPS was presented. Further, a two-way time synchronization algorithm for CPS service composition was put forward. And a formal method, for judging if actual CPS service meets space constraints, was suggested, which was based on space-π-calculus proposed. Finally, a case study was performed and CPS business process designed by the model and the proposed methods could run well. The application of research conclusion implies that it has rationality and feasibility.

Explainable Artificial Intelligence for Workflow Verification in Visual IoT/Robotics Programming Language Environment

Teaching students the concepts behind computational thinking is a difficult task,often gated by the inherent difficulty of programming languages.In the classroom,teaching assistants may be required to interact with students to help them learn the material.Time spent in grading and offering feedback on assignments removes from this time to help students directly.As such,we offer a framework for developing an explainable artificial intelligence that performs automated analysis of student code while offering feedback and partial credit.The creation of this system is dependent on three core components.Those components are a knowledge base,a set of conditions to be analyzed,and a formal set of inference rules.In this paper,we develop such a system for our own language by employing π-calculus and Hoare logic.Our detailed system can also perform self-learning of rules.Given solution files,the system is able to extract the important aspects of the program and develop feedback that explicitly details the errors students make when they veer away from these aspects.The level of detail and expected precision can be easily modified through parameter tuning and variety in sample solutions.

Inference systems for observation equivalences in the π-calculus

Inference systems for observation equivalences in the pi-calculus with recursion are proposed, and their completeness over the finite-control fragment with guarded recursions are proven. The inference systems consist of inference rules and equational axioms. The judgments are conditional equations which characterise symbolic bisimulations between process terms. This result on the one hand generalises Milner’s complete axiomatisation of observation equivalence for regular CCS to the pi-calculus, and on the other hand extends the proof systems of strong bisimulations for guarded regular pi-calculus to observation equivalences.

Describing Service-Oriented Architecture by Extended Darwin

Describing Service-Oriented Architecture （SOA） is critical in the development of Web based system, in this paper, an approach for describing SOA by extended Darwin is proposed. The requirements for describing SOA, which are different from that of ordinary architecture, are highlighted firstly, and then a solution for extending Darwin is presented. Using the extended Darwin, service components and connectors can be described explicit by the extended construct, as well as precise operational semantics of SOA by the π-calculus. Finally an example of supply-chain management system is given for manifesting the effect of the extended Darwin.

Process View of Reflection Mechanism for Reuse Software Architecture

Reflection mechanism for reuse software architecture （RMRSA） divides a software architecture into base-level architecture and meta-level architecture logically. Base-level architecture is the ordinary architecture; meta-level represents and manipulates the reusable meta-information of base-level architecture explicitly. Through reflection, the modification of meta-level architecture will result in the modification of the architecture in base-level. Then we can gain a new base-level architecture design. In this paper, we use π-calculus to define the constituents and their interaction processes of RMRSA, by these definition, we specify the business function in base-level at runtime, and illustrate the reflection mechanism between the base-level architecture and meta-level architecture.

Petri nets semantics ofπ-calculus

As π-calculus based on the interleaving semantics cannot depict the true concurrency and has few supporting tools,it is translated into Petri nets.π-calculus is divided into basic elements,sequence,concurrency,choice and recursive modules.These modules are translated into Petri nets to construct a complicated system.Petri nets semantics for π-calculus visualize system structure as well as system behaviors.The structural analysis techniques allow direct qualitative analysis of the system properties on the structure of the nets.Finally,Petri nets semantics for π-calculus are illustrated by applying them to mobile telephone systems.

An Implementation of Pure Horn Clause Logic Programming in a Reduction System

Many reduction systems have been presented for implementing functional programming languages. We propose here an extension of a reduction architecture to realize a kind of logic programming——pure Horn clause logic programming.This is an attempt to approach amalgama- tion of the two important programming paradigms.

Concurrent Calculus (CC) and Its Properties

Concurrent calculus (CC) is a mathematical model for higher-order concurrent and communicating systems. Compared with the existing calculi such as CCS, CMP, CHOCS etc., CC includes λ-calculus as its subtheory and embodies most important characteristics of CCS and other calculi. CC treats processes and communicating ports as firstclass objects, that is to say, both of them can be sent and received during communication. Besides, the communicating ports in CC-processes are allowed to be any expressions. This paper presents the syntax and semantics of CC first, some examples are given which illustrate the expressing power of CC. Then we study the hlgh-order bisimulation equivalence of CC-processes and the algebraic laws of CC. The summation operator "+" in CC has the same meaning as that in other calculi. Following the principle that only environment can determiue the evolution direction of summation process, this paper also provides a new semantics of summation operator "+", which is different from the semantics of summation in CCS, CMP, and CHOCS. CC has some expected algebraic properties under this new semantics of summation.

Y_CΩ_(2n)are easy terms

For any natural number n≥1, Y CΩ 2n is an easy term; that is, for any λ term M, λβ+Y\-CΩ 2n =M is consistent, where Y C is Curry fixed point combinator, Ω 2n ≡ω 2n ω 2n and ω 2n ≡λx.xx...x (there are 2n occurrences of x after λx ). This result is a partial solution to Jacopini’s conjecture: Y CΩ n is an easy term for any natural number n≥2.

Model Checking Real-Time Value-Passing Systems

In this paper, to model check real-time value-passing systems, a formallanguage Timed Symbolic Transition Graph and a logic system named Timed Predicate μ-Calculus areproposed. An algorithm is presented which is local in that it generates and investigates thereachable state space in top-down fashion and maintains the partition for time evaluations as coarseas possible while on-the-fly instantiating data variables. It can deal with not only data variableswith finite value domain, but also the so called data independent variables with infinite valuedomain. To authors knowledge, this is the first algorithm for model checking timed systemscontaining value-passing features.

A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.

Process Passing Calculus,Revisited

In the context of process calculi, higher order π calculus （A calculus） is prominent and popular due to its ability to transfer processes. Motivated by the attempt to study the process theory in an integrated way, we give a system study of A calculus with respect to the model independent framework. We show the coincidence of the context bisimulation to the absolute equality. We also build a subbisimilarity relation from A calculus to the π calculus.

A Formal Semantics for DAI Language NUML

Traditional AI systems are brittle in the sense that they fail miserably whenpresented with problems even slightly outside of their limited range of expertise.A powerful, extensible strategy of Distributed Artificial Intelligence (DAI) forovercoming such bounds is to put the system in a society of systems. So theability to coordinate group activities of individuals and to communicate betweeneach other is necessary for a language describing DAI systems. Agent-orientedlanguage NUML is such a language. It is a specific kind of object-orientedlanguage. To give formal semantics to NUML, there is the problem to for-malise object-oriented programming paradigm which is still open. The theoryof higher-order rr-calculus is a concurrent computation model with sufficientcapability, which provides us a mathematical tool to do the formalization. Thispaper tries to use higher-order T-calculus to formalise NUML.

A Syntactic Proofof the Conservativity of λ_ω over λ_2

In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.