Regular disjunction-free default theories
In this paper, the class of regular disjunction-free default theories is introduced and investigated. A transformation from regular default theories to normal default theories is established. The initial theory and the transformed theory have the same extensions when restricted to old variables. Hence, regular default theories enjoy some similar properties (e.g., existence of extensions, semi-monotonicity) as normal default theories. Then, a new algorithm for credulous reasoning of regular theories is developed. This algorithm runs in a time not more thanO(1. 45n), wheren is the number of defaults. In case of regular prerequisite-free or semi-2CNF default theories, the credulous reasoning can be solved in polynomial time. However, credulous reasoning for semi-Horn default theories is shown to be NP-complete although it is tractable for Horn default theories. Moreover, skeptical reasoning for regular unary default theories is co-NP-complete.

title: Fixed-parameter tractability of disjunction-free default reasoning
abstract: In this paper, the parameter which is the source of the complexity of disjunction-free default reasoning is determined. It is shown that when the value of this parameter is fixed, the disjunction-free default reasoning can be solved in time bounded by a polynomial whose degree does not depend on the parameter. Consequently, disjunction-free default reasoning is fixed parameter tractable.

title: Polynomial time algorithms for computing a representation for minimal unsatisfiable formulas with fixed deficiency
abstract: We say a propositional formula F in conjunctive normal form is represented by a formula H and a homomorphism φ, if φ(H) = F. A homomorphism is a mapping consisting of a renaming and an identification of literals. The deficiency of a formula is the difference between the number of clauses and the number of variables. We show that for fixed k ≥ 1 and t ≥ 1 each minimal unsatisfiable formula with deficiency k can be represented by a formula H with deficiency t and a homomorphism and such a representation can be computed in polynomial time.

title: Some Algorithms for Extension Computation of Nonmonotonic Rule Systems
abstract: In this paper, we will place our emphasis on the problem of existence of extensions and on finding more efficient algorithms for computing extensions of nonmonotonic rule systems. First, in order to dedicate further research into nonmonotonic rule systems a new characterization and some new results are given. This characterization and these results lead to new algorithms for computing extensions. Second, a class of nonmonotonic rule systems, called regular nonmonotonic rule systems, is developed. The existence of extensions and semi-monotonicity of regular nonmonotonic rule systems are proved. Third, we prove that each regular nonmonotonic rule system has at most 1.47^n extensions, where n is the number of elements occurring in the system.

title: On Boolean Models for Quantified Boolean Horn Formulas
abstract: For a Quantified Boolean Formula \(({\it QBF })\) Φ=Qφ, an assignment is a function \(\cal M\) that maps each existentially quantified variable of Φ to a Boolean function, where φ is a propositional formula and Q is a linear ordering of quantifiers on the variables of Φ. An assignment \(\cal M\) is said to be proper, if for each existentially quantified variable y i , the associated Boolean function f i does not depend upon the universally quantified variables whose quantifiers in Q succeed the quantifier of y i . An assignment \(\cal M\) is said to be a model for Φ, if it is proper and the formula \(\phi^{\cal M}\) is a tautology, where \(\phi^{\cal M}\) is the formula obtained from φ by substituting f i for each existentially quantified variable y i . We show that any true quantified Horn formula has a Boolean model consisting of monotone monomials and constant functions only; conversely, if a QBF has such a model then it contains a clause–subformula in \({\it QHORN }\cap {\it SAT }\).

title: On the structure of some classes of minimal unsatisfiable formulas
abstract: We investigate classes of minimal unsatisfiable formulas which are closed under splitting. For marginal formulas the equivalence to some natural classes of formulas is proved. Further, we show that maximal formulas are closely related to the so-called hitting formulas. That are formulas for which any two clauses contain a pair of complementary literals.

title: Flexible network support for mobility
abstract: Fueled by the large number of powerful tight-weight portable computers, the expanding availability of wirel= networks, and the popularity of the Internet, there is an increasing de mand to connect portable computers to the Internet at any time and in any place. However, the dynamic nature of such connectivity requires more flexible network support than has typically been atiable for stationary workstations. ThM paper introducw the following two me~anisms, in the context of Mobile 1P [24], to ensure a mobile host’s convenient and efficient communication with other hosts in a &anging environment. One me&anism supports multiple packet defivery methods (such as regular 1P or Mobile 1P) and adaptively selects the most appropriate one to use Wcordlng to the char=teristim of eti trfic flow. The other medanism enables a mobile host to make use of multiple wtive network interfww simultaneously and to control the selection of the most dwirable network interfaces for both outgoing and incoming pdets for different traffic flows. We demonstrate the usefdnm of these two network layer me&anisms and describe how they are implemented.

title: Towards the Semantics and Verification of BPEL4WS
abstract: In this paper, we discuss the semantics of BPEL4WS language which is a de facto standard for specifying and execution workflow specification for web service composition and orchestration. We propose a language @m-BPEL that includes most primitive and structured activities of BPEL4WS, and define its semantics. As the Timed Automata (TA) is powerful in designing real-time models with multiple clocks and has well developed automatic tool support, we define a map from @m-BPEL into composable TA. Therefore, the properties we want to check can be verified in TA network correspondingly. Furthermore, we prove that the mapping from @m-BPEL to TA is a simulation, which means that the TA network simulates correctly the corresponding @m-BPEL specification. The case study with model checker Uppaal shows that our method is effective, and a Java supporting tool based on Uppaal model checker engine has been developed.

title: Model Checking Dynamic UML Consistency
abstract: UML is widely accepted and extensively used in software modeling. However, using different diagrams to model different aspects of a system brings the risk of inconsistency among diagrams. In this paper, we investigate an approach to check the consistency between the sequence diagrams and statechart diagrams using the SPIN model checker. To deal with the hierarchy structure of statechart diagrams, we propose a formalism called Split Automata, a variant of automata, which is helpful to bridge the statechart diagrams to SPIN efficiently. Compared with the existing work on model checking UML which do not have formal verification for their translation from UML to the model checker, we formally define the semantics and prove that the automatically translated model (i.e. Split Automata) does simulate the UML model. In this way, we can guarantee that the translated model does represent the original model.

title: Towards the Formal Model and Verification of Web Service Choreography Description Language
abstract: The Web Services Choreography Description Language (WS-CDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. For the rigorous development and tools support for the language, the formal semantics of WS-CDL is worth investigating. This paper proposes a small language CDL as a formal model of the simplified WSCDL, which includes important concepts related to participant roles and collaborations among them in a choreography. The formal operational semantics of CDL is given. Based on the formal model, we discuss further: 1) project a given choreography to orchestration views, which provides a basis for the implementation of the choreography by code generation; 2) translate WS-CDL to the input language of the model-checker SPIN, which allows us to automatically verify the correctness of a given choreography. An automatic translator has been implemented.

title: Towards the theoretical foundation of choreography
abstract: With the growth of interest on the web services, people pay increasinglyattention to the choreography, that is, to describe collaborations ofparticipants in accomplishing a common business goal from a globalviewpoint. In this paper, based on a simple choreography language and arole-oriented process language, we study some fundamental issues relatedto choreography, especially those related to implementation, includingsemantics, projection and natural projection, dominant role in choices anditerations, etc. We propose the concept of dominant role and somenovel languages structures related to it. The study reveals some cluesabout the language, the semantics, the specification and theimplementation of choreography.