5268865
On the structure of some classes of minimal unsatisfiable formulas
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.
8778857
On Models for Quantified Boolean Formulas
A quantified Boolean formula is true, if for any existentially quantified variable there exists a Boolean function depending on the preceding universal variables, such that substituting the existential variables by the Boolean functions results in a true formula. We call a satisfying set of Boolean functions a model. In this paper, we investigate for various classes of quantified Boolean formulas and various classes of Boolean functions the problem whether a model exists. Furthermore, for these classes the complexity of the model checking problem – whether a set of Boolean functions is a model for a formula – will be shown. Finally, for classes of Boolean functions we establish some characterizations in terms of quantified Boolean formulas which have such a model. For example, roughly speaking any satisfiable quantified Boolean Horn formula can be satisfied by monomials and vice versa.
30011892
Complexity of argument-based default reasoning with specificity
In this paper we investigate the complexity of Dung and Son's approach to default reasoning with specificity. We show that the three decision problems: existence of extensions, brave reasoning and cautious reasoning are generally complete for the second level of the polynomial hierarchy. For some restricted cases, e.g., Horn and 2CNF default theories, all the three problems are intractable although classical brave reasoning in these cases is tractable. Finally, we show that stratification can not reduce the complexity of brave and cautious reasoning although it guarantees the existence of extensions.
32094146
On Boolean Models for Quantified Boolean Horn Formulas
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 }\).
7900372
Complexity of the Unique Extension Problem in Default Logic
In this paper we analyze the problem of checking whether a default theory has a single extension. This problem is important for at least three reasons. First, if a theory has a single extension, nonmonotonic inference can be reduced to entailment in propositional logic (which is computationally easier) using the set of consequences of the generating defaults. Second, a theory with many extensions is typically weak i.e., it has few consequences; this indicates that the theory is of little use, and that new information has to be added to it, either as new formulae, or as preferences over defaults. Third, some applications require as few extensions as possible (e.g. diagnosis). We study the complexity of checking whether a default theory has a single extension. We consider the combination of several restrictions of default logics: seminormal, normal, disjunction-free, unary, ordered. Complexity varies from the first to the third level of the polynomial hierarchy. The problem of checking whether a theory has a given number of extensions is also discussed.
1096538
Complexity Results for 2CNF Default Theories
This paper is concerned with the complexity of default reasoning with 2CNF default theories (D,W) in which W is a set of literals and D is a set of 2CNF defaults. It is proved that the problem whether a literal occurs in at least one extension can be solved in polynomial time. But the problem whether a literal appears in all extensions is proved to be co-NP-complete. The complexity of some subclasses of 2CNF default theories is also analyzed.
2194617
Model Checking Dynamic UML Consistency
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.
33266884
Flexible Network Support for Mobile Hosts
Fueled by the large number of powerful light-weight portable computers, the expanding availability of wireless networks, and the popularity of the Internet, there is an increasing demand to connect portable computers to the Internet at any time and in any place. However, the dynamic nature of a mobile host's connectivity and its use of multiple network interfaces require more flexible network support than has typically been available for stationary workstations.This paper introduces two flow-oriented mechanisms, in the context of Mobile IP , to ensure a mobile host's robust and efficient communication with other hosts in a changing environment. One mechanism supports multiple packet delivery methods (such as regular IP or Mobile IP) and adaptively selects the most appropriate one to use according to the characteristics of each traffic flow. The other mechanism enables a mobile host to make use of multiple network interfaces simultaneously and to control the selection of the most desirable network interfaces for both outgoing and incoming packets for different traffic flows. We demonstrate the usefulness of these two network layer mechanisms and describe their implementation and performance.
16590593
An approach to hardware/software partitioning for multiple hardware devices model
Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for multiple hardware-devices model. The partitioning is transformed into a reachability problem of timed automata, and the optimal solution can be obtained by means of an optimal reachability algorithm. To relax the initial condition of partitioning for optimization, two algorithms are designed to explore the dependency relations among processes in the sequential specification. Some experiments are conducted with model checker UPPAAL to show our approach is both effective and efficient.
1661187
Siren: catching evasive malware
With the growing popularity of anomaly detection systems, which is due partly to the rise in zero-day attacks, a new class of threats have evolved where the attacker mimics legitimate activity to blend in and avoid detection. We propose a new system called Siren that injects crafted human input alongside legitimate user activity to thwart these mimicry attacks. The crafted input is specially designed to trigger a known sequence of network requests, which Siren compares to the actual traffic. It then flags unexpected messages as malicious. Using this method, we were able to detect ten spyware programs that we tested, many of which attempt to blend in with user activity. This paper presents the design, implementation, and evaluation of the Siren activity injection system, as well as a discussion of its potential limitations
12052255
Flexible network support for mobility
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.