Barbed Congruence of Asymmetry and Mismatch

The X calculus is a model of concurrent and mobile systems. It emphasizes that communications are information exchanges. In the paper, two constructions are incorporated into the framework of the chi calculus, which are asymmetric communication and mismatch condition widely used in applications. Since the barbed bisimilarity has proved its generality and gained its popularity as an effective approach to generating a reasonable observational equivalence, we study both the operational and algebraic properties of the barbed bisimilarity in this enriched calculus. The investigation supports an improved understanding of the bisimulation behaviors of the model. It also gives a general picture of how the two constructions affect the observational theory.     

A functional presentation of Pi calculus

From the very beginning process algebra introduced the dichotomy between channels and processes. This dichotomy prevails in all present process calculi. The situation is in contrast to that withlambda calculus which has only one class of entities-the lambda terms. We introduce in this papera process calculus called Lamp in which channels are process names. The language is more uniform than existing process calculi in two aspects-. First it has a unified treatment of channels and processes.There is only one class of syntactical entities-processes. Second it has a unified presentation ofboth first order and higher order process calculi. The language is functional in the sense that lambda calculus is functional. Two bisimulation equivalences, barbed and closed bisimilarities, are proved to coincide.A natural translation from Pi calculus to Lamp is shown to preserve both operational and algebraic semantics. The relationship between lazy lambda calculus and Lamp is discussed.     

On controllability and stabilizability of probabilistic Boolean control networks

The controllability of probabilistic Boolean control networks(PBCNs)is first considered.Using the input-state incidence matrices of all models,we propose a reachability matrix to characterize the joint reachability.Then we prove that the joint reachability and the controllability of PBCNs are equivalent,which leads to a necessary and sufcient condition of the controllability.Then,the result of controllability is used to investigate the stability of probabilistic Boolean networks(PBNs)and the stabilization of PBCNs.A necessary and sufcient condition for the stability of PBNs is obtained first.By introducing the control-fixed point of Boolean control networks(BCNs),the stability condition has finally been developed into a necessary and sufcient condition of the stabilization of PBCNs.Both necessary and sufcient conditions for controllability and stabilizability are based on reachability matrix,which are easily computable.Hence the two necessary and sufcient conditions are straightforward verifiable.Numerical examples are provided from case to case to demonstrate the corresponding theoretical results.     

RAO logic for multiagent framework

In this paper,we deal with how agents reason about knowledge of others in multiagent system.We first present a knowledge representation framework called reasoning about others(RAO) which is designed specifically to represent concepts and rules used in reasoning about knowledge of others.From a class of sentences usually taken by people in daily life to reason about others,a rule called position exchange principle(PEP)is abstracted.PEP is described as an axiom scheme in RAO and regarded as a basic rule for agents to reason about others,and further it has the similar form and role to modus ponens and(K) axion of knowledge logic.The relationship between speech acts and common sense is also discussed which is necessary for RAO.Based on ideas from situation calculus,this relationship is characterized by an axiom schema in RAO.Our theories are also demonstrated by an example.     

On Isomorphism Testing of Groups with Normal Hall Subgroups

A normal Hall subgroup N of a group G is a normal subgroup with its order coprime with its index.SchurZassenhaus theorem states that every normal Hall subgroup has a complement subgroup,that is a set of coset representatives H which also forms a subgroup of G.In this paper,we present a framework to test isomorphism of groups with at least one normal Hall subgroup,when groups are given as multiplication tables.To establish the framework,we first observe that a proof of Schur-Zassenhaus theorem is constructive,and formulate a necessary and sufficient condition for testing isomorphism in terms of the associated actions of the semidirect products,and isomorphisms of the normal parts and complement parts.We then focus on the case when the normal subgroup is abelian.Utilizing basic facts of representation theory of finite groups and a technique by Le Gall (STACS 2009),we first get an efficient isomorphism testing algorithm when the complement has bounded number of generators.For the case when the complement subgroup is elementary abelian,which does not necessarily have bounded number of generators,we obtain a polynomial time isomorphism testing algorithm by reducing to generalized code isomorphism problem,which asks whether two linear subspaces are the same up to permutation of coordinates.A solution to the latter can be obtained by a mild extension of the singly exponential (in the number of coordinates) time algorithm for code isomorphism problem developed recently by Babai et al.(SODA 2011).Enroute to obtaining the above reduction,we study the following computational problem in representation theory of finite groups: given two representations ρ and τ of a group H over Zpd,p a prime,determine if there exists an automorphism φ : H → H ,such that the induced representation ρφ = ρφ and τ are equivalent,in time poly(|H |,pd).     

A development calculus for specifications

A first order inference system, named R-calculus, is defined to develop the specifications. This system intends to eliminate the laws which are not consistent with users' requirements. The R-calculus consists of the structural rules, an axiom, a cut rule, and the rules for logical connectives. Some examples are given to demonstrate the usage of the R-calculus. Furthermore, the properties regarding reachability and completeness of the R-calculus are formally defined and proved.     

An Operational Approach to Belief Revision

A deduction system,called RE-proof system,is constructed for generating the revisions of first order belief sets.When a belief set is rejected by a given fact,all maximal subsets of the belief set consistent with the fact can be deduced from the proof system.The soundness and completeness of the RE-proof system are proved,which imply that there exists a resolution method to decide whether a revision retains a maximal subset of a belief set.     

A representative model based algorithm for maximal contractions

In this paper,we propose a representative model based algorithm to calculate maximal contractions.For a formal theory Γ and a fact set Δ,the algorithm begins by accepting all models of refutation by facts of Γ with respect to Δ and filters these models to obtain the models of R-refutation.According to the completeness of R-calculus,the relevant maximal contraction is obtained simultaneously.In order to improve the efficiency,we divide the models into different classes according to the assignments of atomic propositions and only select relevant representative models to verify the satisfiability of each proposition.The algorithm is correct,and all maximal contractions of a given problem can be calculated by it.Users could make a selection according to their requirements.A benchmark algorithm is also provided.Experiments show that the algorithm has a good performance on normal revision problems.     

Dust collector localization in trouble of moving freight car detection system

For a long time,trouble detection and maintenance of freight cars have been completed manually by inspectors.To realize the transition from manual to computer-based detection and maintenance,we focus on dust collector localization under complex conditions in the trouble of moving freight car detection system.Using mid-level features which are also named flexible edge arrangement(FEA) features,we first build the edge-based 2D model of the dust collectors,and then match target objects by a weighted Hausdorff distance method.The difference is that the constructed weighting function is generated by the FEA features other than specified subjectively,which can truly reflect the most basic property regions of the 3D object.Experimental results indicate that the proposed algorithm has better robustness to variable lighting,different viewing angle,and complex texture,and it shows a stronger adaptive performance.The localization correct rate of the target object is over 90%,which completely meets the need of practical applications.     

Robust network structures for conserving total activity in Boolean networks

One of the typical properties of biological systems is the law of conservation of mass, that is, the property that the mass must remain constant over time in a closed chemical reaction system. However, it is known that Boolean networks, which are a promising model of biological networks, do not always represent the conservation law. This paper thus addresses a kind of conservation law as a generic property of Boolean networks. In particular, we consider the problem of finding network structures on which, for any Boolean operation on nodes, the number of active nodes, i.e., nodes whose state is one, is constant over time. As a solution to the problem, we focus on the strongly-connected network structures and present a necessary and sufficient condition.     

Hoare Logic and Auxiliary Variables

Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the role of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, one can show that Hoare Logic subsumes Vienna Development Method's (VDM) operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion. Received October 1998 / Accepted in revised form October 1999     

Expressiveness and the completeness of Hoare's logic

Three theorems are proven which reconsider the completeness of Hoare's logic for the partial correctness of while-programs equipped with a first-order assertion language. The results are about the expressiveness of the assertion language and the role of specifications in completeness concerns for the logic: (1) expressiveness is not a necessary condition on a structure for its Hoare logic to be complete, (2) complete number theory is the only extension of Peano Arithmetic which yields a logically complete Hoare logic and (3) a computable structure with enumeration is expressive if and only if its Hoare logic is complete.     

The Disconnection Tableau Calculus

In this paper we give a comprehensive presentation of the disconnection tableau calculus, a proof method for formulas in classical first-order clause logic. The distinguishing property of this calculus is that it uses unification in such a manner that important proof-theoretic advantages of the classical (i.e., Smullyan-style) tableau calculus are preserved, specifically the termination and model generation characteristics for certain formula classes. Additionally, the calculus is well suited for fully automated proof search. The calculus is described in detail with soundness and completeness proofs, and a number of important calculus refinements developed over the past years are presented. Referring to the model-finding abilities of the disconnection calculus, we explain the extraction and representation of models. We also describe the integration of paramodulation-based equality handling. Finally, we give an overview of related methods.     

Sequent calculi and decidability for intuitionistic hybrid logic

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.     

Terminating Calculi for Propositional Dummett Logic with Subformula Property

In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the semantical levels of known or not known at the present state of knowledge, that are usual in tableau systems, and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms.     

Process expressions and Hoare's logic: Showing an irreconcilability of context-free recursion with Scott's induction rule

In this paper processes specifiable over a non-uniform language are considered. The language contains constants for a set of atomic actions and constructs for alternative and sequential composition. Furthermore it provides a mechanism for specifying processes recursively (including nested recursion). We consider processes as having a state: atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. Any process having some initial state can be associated with a transition system representing all possible courses of execution. This leads to an operational semantics in the style of Plotkin. The partial correctness assertion {α} p{β} expresses that for any transition system associated with the process p and having some initial state satisfying α, its final states representing successful execution satisfy β. A logic in the style of Hoare, containing a proof system for deriving partial correctness assertions, is presented. This proof system is sound and relatively complete, so any partial correctness assertion can be evaluated by investigating its derivability. Included is a short discussion about the extension of the process language with “guarded recursion”. It appears that such an extension violates the completeness of the Hoare logic. This reveals a remarkable property of Scott's induction rule in the context of non-determinism: only regular recursion allows a completeness result.     

Resolution for Max-SAT

Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule.Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems.     

The verification of modules

We present a module concept with algebraic interfaces and imperative implementation. It is shown that under some natural conditions, module correctness may be expressed in Hoare logic as a partial correctness assertion. Also, we discuss questions of practical verification of modules using Hoare's calculus.     

Verification conditions are code

This paper presents a new theoretical result concerning Hoare Logic. It is shown here that the verification conditions that support a Hoare Logic program derivation are themselves sufficient to construct a correct implementation of the given pre-, and post-condition specification. This property is mainly of theoretical interest, though it is possible that it may have some practical use, for example if predicative programming methodology is adopted. The result is shown to hold for both the original, partial correctness, Hoare logic, and also a variant for total correctness derivations.