## Institut für Informatik und Computational Science

### Refine

#### Year of publication

- 2011 (54) (remove)

#### Document Type

- Article (27)
- Doctoral Thesis (18)
- Monograph/Edited Volume (3)
- Other (2)
- Preprint (2)
- Habilitation (1)
- Review (1)

#### Keywords

- Answer Set Programming (3)
- answer set programming (3)
- Antwortmengenprogrammierung (2)
- Tracking (2)
- Abstraktion (1)
- Accepting Grammars (1)
- Akzeptierende Grammatiken (1)
- Algorithmen (1)
- Algorithms (1)
- Answer set programming (1)
- Antwortmengen Programmierung (1)
- Asynchrone Schaltung (1)
- Automata systems (1)
- Beweistheorie (1)
- Bildverarbeitung (1)
- CP-Logic (1)
- CSC (1)
- CityGML (1)
- Code generation (1)
- Complex optimization (1)
- Computergrafik (1)
- Controlled Derivations (1)
- D-galactosamine (1)
- Decidability (1)
- Entwurfsmuster für SOA-Sicherheit (1)
- Entwurfsraumexploration (1)
- Extreme Model-Driven Development (1)
- FMC-QE (1)
- FPGA (1)
- Gesteuerte Ableitungen (1)
- Grammar Systems (1)
- Grammatiksysteme (1)
- Hardware-Software-Co-Design (1)
- Hierarchically configurable mask register (1)
- IT-Security (1)
- IT-Sicherheit (1)
- Incremental answer set programming (1)
- Inkonsistenz (1)
- Knowledge Representation and Reasoning (1)
- Knowledge representation (1)
- Komplexität (1)
- Komplexitätsbewältigung (1)
- L systems (1)
- Leftmost Derivations (1)
- Leistungsvorhersage (1)
- Linksableitungen (1)
- Localization (1)
- Logiksynthese (1)
- Markov processes (1)
- Masking of X-values (1)
- Meta-Programming (1)
- Model Driven Architecture (1)
- Model checking (1)
- Modell (1)
- Modell-driven Security (1)
- Modell-getriebene Sicherheit (1)
- Modellgetriebene Architektur (1)
- Nutzungsinteresse (1)
- Ontologie (1)
- Ontology (1)
- Operation problem (1)
- Parsing (1)
- Performance Prediction (1)
- Pre-RS Traceability (1)
- Preference Handling (1)
- Process model analysis (1)
- Proof Theory (1)
- Prozess (1)
- Quantitative Modeling (1)
- Quantitative Modellierung (1)
- Queuing Theory (1)
- Reparatur (1)
- SOA Security Pattern (1)
- STG decomposition (1)
- STG-Dekomposition (1)
- Security Modelling (1)
- Semantic Web (1)
- Service-Orientierte Architekturen (1)
- Service-oriented Architectures (1)
- Sicherheitsmodellierung (1)
- Statistical relational learning (1)
- Stochastic relational process (1)
- System Biologie (1)
- Texturen (1)
- Time Augmented Petri Nets (1)
- Time series (1)
- Transformation (1)
- Unary languages (1)
- Unvollständigkeit (1)
- Usage Interest (1)
- Verification (1)
- Warteschlangentheorie (1)
- Web Sites (1)
- Webseite (1)
- Wireless Sensor Networks (1)
- Wissensrepräsentation und -verarbeitung (1)
- Zeitbehaftete Petri Netze (1)
- abstraction (1)
- acute liver failure (1)
- asynchronous circuit (1)
- behavioral abstraction (1)
- bioinformatics (1)
- block representation (1)
- cellular automata (1)
- complexity (1)
- computer graphics (1)
- consistency (1)
- consistency checking (1)
- consistency measures (1)
- cooperating systems (1)
- decidability questions (1)
- declarative problem solving (1)
- design space exploration (1)
- diagnosis (1)
- endothelin (1)
- endothelin-converting enzyme (1)
- finite model computation (1)
- formal languages (1)
- hardware-software-codesign (1)
- image processing (1)
- incompleteness (1)
- inconsistency (1)
- kidney cancer (1)
- logic synthesis (1)
- loop formulas (1)
- metabolism (1)
- metabolomics (1)
- metastasis (1)
- model (1)
- neighborhood (1)
- neutral endopeptidase (1)
- nichtlineare Projektionen (1)
- nonlinear projections (1)
- on-chip (1)
- process (1)
- process model alignment (1)
- quantum (1)
- repair (1)
- semantisches Netz (1)
- speed independence (1)
- stable model semantics (1)
- systems biology (1)
- textures (1)
- transformation (1)
- unfounded sets (1)
- virtual 3D city models (1)
- virtuelle 3D-Stadtmodelle (1)

We define and study quantum cellular automata (QCA). We show that they are reversible and that the neighborhood of the inverse is the opposite of the neighborhood. We also show that QCA always admit, modulo shifts, a two-layered block representation. Note that the same two-layered block representation result applies also over infinite configurations, as was previously shown for one-dimensional systems in the more elaborate formalism of operators algebras [18]. Here the proof is simpler and self-contained, moreover we discuss a counterexample QCA in higher dimensions.

Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover.

Parsability approaches of several grammar formalisms generating also non-context-free languages are explored. Chomsky grammars, Lindenmayer systems, grammars with controlled derivations, and grammar systems are treated. Formal properties of these mechanisms are investigated, when they are used as language acceptors. Furthermore, cooperating distributed grammar systems are restricted so that efficient deterministic parsing without backtracking becomes possible. For this class of grammar systems, the parsing algorithm is presented and the feature of leftmost derivations is investigated in detail.

We investigate the decidability of the operation problem for TOL languages and subclasses. Fix an operation on formal languages. Given languages from the family considered (OL languages, TOL languages, or their propagating variants), is the application of this operation to the given languages still a language that belongs to the same language family? Observe, that all the Lindenmayer language families in question are anti-AFLs, that is, they are not closed under homomorphisms, inverse homomorphisms, intersection with regular languages, union, concatenation, and Kleene closure. Besides these classical operations we also consider intersection and substitution, since the language families under consideration are not closed under these operations, too. We show that for all of the above mentioned language operations, except for the Kleene closure, the corresponding operation problems of OL and TOL languages and their propagating variants are not even semidecidable. The situation changes for unary OL languages. In this case we prove that the operation problems with respect to Kleene star, complementation, and intersection with regular sets are decidable.

Parallel communicating finite automata (PCFAs) are systems of several finite state automata which process a common input string in a parallel way and are able to communicate by sending their states upon request. We consider deterministic and nondeterministic variants and distinguish four working modes. It is known that these systems in the most general mode are as powerful as one-way multi-head finite automata. It is additionally known that the number of heads corresponds to the number of automata in PCFAs in a constructive way. Thus, undecidability results as well as results on the hierarchies induced by the number of heads carry over from multi-head finite automata to PCFAs in the most general mode. Here, we complement these undecidability and hierarchy results also for the remaining working modes. In particular, we show that classical decidability questions are not semi-decidable for any type of PCFAs under consideration. Moreover, it is proven that the number of automata in the system induces infinite hierarchies for deterministic and nondeterministic PCFAs in three working modes.

Recent evidence suggests that metabolic changes play a pivotal role in the biology of cancer and in particular renal cell carcinoma (RCC). Here, a global metabolite profiling approach was applied to characterize the metabolite pool of RCC and normal renal tissue. Advanced decision tree models were applied to characterize the metabolic signature of RCC and to explore features of metastasized tumours. The findings were validated in a second independent dataset. Vitamin E derivates and metabolites of glucose, fatty acid, and inositol phosphate metabolism determined the metabolic profile of RCC. alpha-tocopherol, hippuric acid, myoinositol, fructose-1-phosphate and glucose-1-phosphate contributed most to the tumour/normal discrimination and all showed pronounced concentration changes in RCC. The identified metabolic profile was characterized by a low recognition error of only 5% for tumour versus normal samples. Data on metastasized tumours suggested a key role for metabolic pathways involving arachidonic acid, free fatty acids, proline, uracil and the tricarboxylic acid cycle. These results illustrate the potential of mass spectroscopy based metabolomics in conjunction with sophisticated data analysis methods to uncover the metabolic phenotype of cancer. Differentially regulated metabolites, such as vitamin E compounds, hippuric acid and myoinositol, provide leads for the characterization of novel pathways in RCC.

We introduce hierarchical kFOIL as a simple extension of the multitask kFOIL learning algorithm. The algorithm first learns a core logic representation common to all tasks, and then refines it by specialization on a per-task basis. The approach can be easily generalized to a deeper hierarchy of tasks. A task clustering algorithm is also proposed in order to automatically generate the task hierarchy. The approach is validated on problems of drug-resistance mutation prediction and protein structural classification. Experimental results show the advantage of the hierarchical version over both single and multi task alternatives and its potential usefulness in providing explanatory features for the domain. Task clustering allows to further improve performance when a deeper hierarchy is considered.

Building biological models by inferring functional dependencies from experimental data is an important issue in Molecular Biology. To relieve the biologist from this traditionally manual process, various approaches have been proposed to increase the degree of automation. However, available approaches often yield a single model only, rely on specific assumptions, and/or use dedicated, heuristic algorithms that are intolerant to changing circumstances or requirements in the view of the rapid progress made in Biotechnology. Our aim is to provide a declarative solution to the problem by appeal to Answer Set Programming (ASP) overcoming these difficulties. We build upon an existing approach to Automatic Network Reconstruction proposed by part of the authors. This approach has firm mathematical foundations and is well suited for ASP due to its combinatorial flavor providing a characterization of all models explaining a set of experiments. The usage of ASP has several benefits over the existing heuristic algorithms. First, it is declarative and thus transparent for biological experts. Second, it is elaboration tolerant and thus allows for an easy exploration and incorporation of biological constraints. Third, it allows for exploring the entire space of possible models. Finally, our approach offers an excellent performance, matching existing, special-purpose systems.

Answer Set Programming (ASP) is an emerging paradigm for declarative programming, in which a computational problem is specified by a logic program such that particular models, called answer sets, match solutions. ASP faces a growing range of applications, demanding for high-performance tools able to solve complex problems. ASP integrates ideas from a variety of neighboring fields. In particular, automated techniques to search for answer sets are inspired by Boolean Satisfiability (SAT) solving approaches. While the latter have firm proof-theoretic foundations, ASP lacks formal frameworks for characterizing and comparing solving methods. Furthermore, sophisticated search patterns of modern SAT solvers, successfully applied in areas like, e.g., model checking and verification, are not yet established in ASP solving. We address these deficiencies by, for one, providing proof-theoretic frameworks that allow for characterizing, comparing, and analyzing approaches to answer set computation. For another, we devise modern ASP solving algorithms that integrate and extend state-of-the-art techniques for Boolean constraint solving. We thus contribute to the understanding of existing ASP solving approaches and their interconnections as well as to their enhancement by incorporating sophisticated search patterns. The central idea of our approach is to identify atomic as well as composite constituents of a propositional logic program with Boolean variables. This enables us to describe fundamental inference steps, and to selectively combine them in proof-theoretic characterizations of various ASP solving methods. In particular, we show that different concepts of case analyses applied by existing ASP solvers implicate mutual exponential separations regarding their best-case complexities. We also develop a generic proof-theoretic framework amenable to language extensions, and we point out that exponential separations can likewise be obtained due to case analyses on them. We further exploit fundamental inference steps to derive Boolean constraints characterizing answer sets. They enable the conception of ASP solving algorithms including search patterns of modern SAT solvers, while also allowing for direct technology transfers between the areas of ASP and SAT solving. Beyond the search for one answer set of a logic program, we address the enumeration of answer sets and their projections to a subvocabulary, respectively. The algorithms we develop enable repetition-free enumeration in polynomial space without being intrusive, i.e., they do not necessitate any modifications of computations before an answer set is found. Our approach to ASP solving is implemented in clasp, a state-of-the-art Boolean constraint solver that has successfully participated in recent solver competitions. Although we do here not address the implementation techniques of clasp or all of its features, we present the principles of its success in the context of ASP solving.

Preference handling and optimization are indispensable means for addressing nontrivial applications in Answer Set Programming (ASP). However, their implementation becomes difficult whenever they bring about a significant increase in computational complexity. As a consequence, existing ASP systems do not offer complex optimization capacities, supporting, for instance, inclusion-based minimization or Pareto efficiency. Rather, such complex criteria are typically addressed by resorting to dedicated modeling techniques, like saturation. Unlike the ease of common ASP modeling, however, these techniques are rather involved and hardly usable by ASP laymen. We address this problem by developing a general implementation technique by means of meta-prpogramming, thus reusing existing ASP systems to capture various forms of qualitative preferences among answer sets. In this way, complex preferences and optimization capacities become readily available for ASP applications.

Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53-65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53-87). Like an Ha: program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.

We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection.

We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reactions and high-throughput profiles of cell activity. We then present an approach based on answer set programming to check the consistency of large-scale data sets. Moreover, we extend this methodology to provide explanations for inconsistencies by determining minimal representations of conflicts. In practice, this can be used to identify unreliable data or to indicate missing reactions.