Searcharxiv⌕ Search

arXiv subjects

Henning Schnoor

Publications and source records attributed to Henning Schnoor.

18 recordsLinked to original sources
arXiv2019

Comparing Static and Dynamic Weighted Software Coupling Metrics

Coupling metrics are an established way to measure software architecture quality with respect to modularity. Static coupling metrics are obtained from the source or compiled code of a program, while dynamic metrics use runtime data gathered e.g., by monitoring a system in production. We study \emph{weighted} dynamic coupling that takes into account how often a connection is executed during a system's run. We investigate the correlation between dynamic weighted metrics and their static counterparts. We use data collected from four different experiments, each monitoring production use of a commercial software system over a period of four weeks. We observe an unexpected level of correlation between the static and the weighted dynamic case as well as revealing differences between class- and package-level analyses.

cs.SE↗
arXiv2016

Complexity Dichotomies for Unweighted Scoring Rules

Scoring systems are an extremely important class of election systems. We study the complexity of manipulation, constructive control by deleting voters (CCDV), and bribery for scoring systems. For manipulation, we show that for all scoring rules with a constant number of different coefficients, manipulation is in P. And we conjecture that there is no dichotomy theorem. On the other hand, we obtain dichotomy theorems for CCDV and bribery problem. More precisely, we show that both of these problems are easy for 1-approval, 2-approval, 1-veto, 2-veto, 3-veto, generalized 2-veto, and (2,1,...,1,0), and hard in all other cases. These results are the "dual" of the dichotomy theorem for the constructive control by adding voters (CCAV) problem from (Hemaspaandra, Hemaspaandra, Schnoor, AAAI 2014), but do not at all follow from that result. In particular, proving hardness for CCDV is harder than for CCAV since we do not have control over what the controller can delete, and proving easiness for bribery tends to be harder than for control, since bribery can be viewed as control followed by manipulation.

cs.CC↗
arXiv2015

A Van Benthem Theorem for Modal Team Semantics

The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of first-order logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic MDL and team semantics. We show that modal team logic MTL, extending MDL by classical negation, captures exactly the FO-definable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area.

cs.LO↗
arXiv2014

The Relative Succinctness and Expressiveness of Modal Logics Can Be Arbitrarily Complex

We study the relative succinctness and expressiveness of modal logics, and prove that these relationships can be as complex as any countable partial order. For this, we use two uniform formalisms to define modal operators, and obtain results on succinctness and expressiveness in these two settings. Our proofs are based on formula size games introduced by Adler and Immerman and bisimulations.

cs.LO↗
arXiv2014

A Control Dichotomy for Pure Scoring Rules

Scoring systems are an extremely important class of election systems. A length-$m$ (so-called) scoring vector applies only to $m$-candidate elections. To handle general elections, one must use a family of vectors, one per length. The most elegant approach to making sure such families are "family-like" is the recently introduced notion of (polynomial-time uniform) pure scoring rules [Betzler and Dorn 2010], where each scoring vector is obtained from its precursor by adding one new coefficient. We obtain the first dichotomy theorem for pure scoring rules for a control problem. In particular, for constructive control by adding voters (CCAV), we show that CCAV is solvable in polynomial time for $k$-approval with $k \leq 3$, $k$-veto with $k \leq 2$, every pure scoring rule in which only the two top-rated candidates gain nonzero scores, and a particular rule that is a "hybrid" of 1-approval and 1-veto. For all other pure scoring rules, CCAV is NP-complete. We also investigate the descriptive richness of different models for defining pure scoring rules, proving how more rule-generation time gives more rules, proving that rationals give more rules than do the natural numbers, and proving that some restrictions previously thought to be "w.l.o.g." in fact do lose generality.

cs.GT↗
arXiv2014

Active Linkability Attacks

We study linking attacks on communication protocols. We show that an active attacker is strictly more powerful in this setting than previously-considered passive attackers. We introduce a formal model to reason about active linkability attacks, formally define security against these attacks and give very general conditions for both security and insecurity of protocols. In addition, we introduce a composition-like technique that allows to obtain security proofs by only studying small components of a protocol.

cs.CR↗
arXiv2014

On Defendability of Security Properties

We study the security of interaction protocols when incentives of participants are taken into account. We begin by formally defining correctness of a protocol, given a notion of rationality and utilities of participating agents. Based on that, we propose how to assess security when the precise incentives are unknown. Then, the security level can be defined in terms of defender sets, i.e., sets of participants who can effectively "defend" the security property as long as they are in favor of the property. We present some theoretical characterizations of defendable protocols under Nash equilibrium, first for bijective games (a standard assumption in game theory), and then for games with non-injective outcomes that better correspond to interaction protocols. Finally, we apply our concepts to analyze fairness in the ASW contract-signing protocol.

cs.CR↗
arXiv2014

Modal Independence Logic

This paper introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of Väänänen's modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms. We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL. We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.

cs.LO↗
arXiv2013

Complexity and Unwinding for Intransitive Noninterference

The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable, as is checking ITO-security (van der Meyden). The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also lead to new unwinding proof techniques that are shown to be sound and complete for these notions of security, and enable the algorithms to return simple counter-examples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.

cs.CR↗
arXiv2013

Noninterference with Local Policies

We develop a theory for state-based noninterference in a setting where different security policies---we call them local policies---apply in different parts of a given system. Our theory comprises appropriate security definitions, characterizations of these definitions, for instance in terms of unwindings, algorithms for analyzing the security of systems with local policies, and corresponding complexity results.

cs.CR↗
arXiv2013

Relation-algebraic and Tool-supported Control of Condorcet Voting

We present a relation-algebraic model of Condorcet voting and, based on it, relation-algebraic solutions of the constructive control problem via the removal of voters. We consider two winning conditions, viz. to be a Condorcet winner and to be in the (Gilles resp. upward) uncovered set. For the first condition the control problem is known to be NP-hard; for the second condition the NP-hardness of the control problem is shown in the paper. All relation-algebraic specifications we will develop in the paper immediately can be translated into the programming language of the BDD-based computer system RelView. Our approach is very flexible and especially appropriate for prototyping and experimentation, and as such very instructive for educational purposes. It can easily be applied to other voting rules and control problems.

cs.GT↗
arXiv2011

A Simplest Undecidable Modal Logic

Modal logics are widely used in computer science. The complexity of their satisfiability problems has been an active field of research since the 1970s. We prove that even very "simple" modal logics can be undecidable: We show that there is an undecidable modal logic that can be obtained by restricting the allowed models with a first-order formula in which only universal quantifiers appear.

cs.LO↗
arXiv2011

Minimization for Generalized Boolean Formulas

The minimization problem for propositional formulas is an important optimization problem in the second level of the polynomial hierarchy. In general, the problem is Sigma-2-complete under Turing reductions, but restricted versions are tractable. We study the complexity of minimization for formulas in two established frameworks for restricted propositional logic: The Post framework allowing arbitrarily nested formulas over a set of Boolean connectors, and the constraint setting, allowing generalizations of CNF formulas. In the Post case, we obtain a dichotomy result: Minimization is solvable in polynomial time or coNP-hard. This result also applies to Boolean circuits. For CNF formulas, we obtain new minimization algorithms for a large class of formulas, and give strong evidence that we have covered all polynomial-time cases.

cs.CC↗
arXiv2009

The Complexity of Generalized Satisfiability for Linear Temporal Logic

In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper undertakes a systematic study of satisfiability for LTL formulae over restricted sets of propositional and temporal operators. Since every propositional operator corresponds to a Boolean function, there exist infinitely many propositional operators. In order to systematically cover all possible sets of them, we use Post's lattice. With its help, we determine the computational complexity of LTL satisfiability for all combinations of temporal operators and all but two classes of propositional functions. Each of these infinitely many problems is shown to be either PSPACE-complete, NP-complete, or in P.

cs.LO↗
arXiv2008

The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments

In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper systematically studies the model-checking problem for LTL formulae over restricted sets of propositional and temporal operators. For almost all combinations of temporal and propositional operators, we determine whether the model-checking problem is tractable (in P) or intractable (NP-hard). We then focus on the tractable cases, showing that they all are NL-complete or even logspace solvable. This leads to a surprising gap in complexity between tractable and intractable cases. It is worth noting that our analysis covers an infinite set of problems, since there are infinitely many sets of propositional operators.

cs.LO↗
arXiv2008

Generalized Modal Satisfiability

It is well known that modal satisfiability is PSPACE-complete (Ladner 1977). However, the complexity may decrease if we restrict the set of propositional operators used. Note that there exist an infinite number of propositional operators, since a propositional operator is simply a Boolean function. We completely classify the complexity of modal satisfiability for every finite set of propositional operators, i.e., in contrast to previous work, we classify an infinite number of problems. We show that, depending on the set of propositional operators, modal satisfiability is PSPACE-complete, coNP-complete, or in P. We obtain this trichotomy not only for modal formulas, but also for their more succinct representation using modal circuits. We consider both the uni-modal and the multi-modal case, and study the dual problem of validity as well.

cs.CC↗
arXiv2008

On the Complexity of Elementary Modal Logics

Modal logics are widely used in computer science. The complexity of modal satisfiability problems has been investigated since the 1970s, usually proving results on a case-by-case basis. We prove a very general classification for a wide class of relevant logics: Many important subclasses of modal logics can be obtained by restricting the allowed models with first-order Horn formulas. We show that the satisfiability problem for each of these logics is either NP-complete or PSPACE-hard, and exhibit a simple classification criterion. Further, we prove matching PSPACE upper bounds for many of the PSPACE-hard logics.

cs.CC↗