TY - GEN A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Special issue on answer set programming T2 - Künstliche Intelligenz Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0554-8 SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 101 EP - 103 PB - Springer CY - Heidelberg ER - TY - GEN A1 - Frank, Mario A1 - Kreitz, Christoph T1 - A theorem prover for scientific and educational purposes T2 - Electronic proceedings in theoretical computer science N2 - We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education. Y1 - 2018 U6 - https://doi.org/10.4204/EPTCS.267.4 SN - 2075-2180 IS - 267 SP - 59 EP - 69 PB - Open Publishing Association CY - Sydney ER - TY - GEN A1 - Schäpers, Björn A1 - Niemueller, Tim A1 - Lakemeyer, Gerhard A1 - Gebser, Martin A1 - Schaub, Torsten H. T1 - ASP-Based Time-Bounded Planning for Logistics Robots T2 - Twenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS 2018) N2 - Manufacturing industries are undergoing a major paradigm shift towards more autonomy. Automated planning and scheduling then becomes a necessity. The Planning and Execution Competition for Logistics Robots in Simulation held at ICAPS is based on this scenario and provides an interesting testbed. However, the posed problem is challenging as also demonstrated by the somewhat weak results in 2017. The domain requires temporal reasoning and dealing with uncertainty. We propose a novel planning system based on Answer Set Programming and the Clingo solver to tackle these problems and incentivize robot cooperation. Our results show a significant performance improvement, both, in terms of lowering computational requirements and better game metrics. Y1 - 2018 SN - 2334-0835 SN - 2334-0843 SP - 509 EP - 517 PB - ASSOC Association for the Advancement of Artificial Intelligence CY - Palo Alto ER - TY - GEN A1 - Marques de Carvalho, Jackson W. A1 - Jürgensen, Helmut T1 - Flexible Structured Mathematics Notation : IADIS, International Conference Interfaces and Human Computer Interaction, Lisabon, 2007 T2 - Preprint / Universität Potsdam, Institut für Informatik Y1 - 2007 SN - 0946-7580 VL - 2007, 1 PB - Univ. CY - Potsdam ER - TY - GEN A1 - Stöpel, Christoph A1 - Schubert, Wolfgang A1 - Margaria-Steffen, Tiziana T1 - Plug-ins und Dienste : Ansätze zu Bewältigung zeitvarianter Geschäftsprozesse T2 - Preprint / Universität Potsdam, Institut für Informatik Y1 - 2007 SN - 0946-7580 VL - 2007, 2 PB - Univ. CY - Potsdam ER - TY - GEN A1 - Bordihn, Henning A1 - Nagy, Benedek A1 - Vaszil, György T1 - Preface: Non-classical models of automata and applications VIII T2 - RAIRO-Theoretical informatics and appli and applications Y1 - 2018 U6 - https://doi.org/10.1051/ita/2018019 SN - 0988-3754 SN - 1290-385X VL - 52 IS - 2-4 SP - 87 EP - 88 PB - EDP Sciences CY - Les Ulis ER - TY - GEN A1 - Lifschitz, Vladimir A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Interview with Vladimir Lifschitz T2 - Künstliche Intelligenz N2 - This interview with Vladimir Lifschitz was conducted by Torsten Schaub at the University of Texas at Austin in August 2017. The question set was compiled by Torsten Schaub and Stefan Woltran. Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0552-x SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 213 EP - 218 PB - Springer CY - Heidelberg ER - TY - GEN A1 - Brewka, Gerhard A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Interview with Gerhard Brewka T2 - Künstliche Intelligenz N2 - This interview with Gerhard Brewka was conducted by correspondance in May 2018. The question set was compiled by Torsten Schaub and Stefan Woltran. Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0549-5 SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 219 EP - 221 PB - Springer CY - Heidelberg ER - TY - GEN A1 - Przybylla, Mareen T1 - Interactive objects in physical computing and their role in the learning process T2 - Constructivist foundations N2 - The target article discusses the question of how educational makerspaces can become places supportive of knowledge construction. This question is too often neglected by people who run makerspaces, as they mostly explain how to use different tools and focus on the creation of a product. In makerspaces, often pupils also engage in physical computing activities and thus in the creation of interactive artifacts containing embedded systems, such as smart shoes or wristbands, plant monitoring systems or drink mixing machines. This offers the opportunity to reflect on teaching physical computing in computer science education, where similarly often the creation of the product is so strongly focused upon that the reflection of the learning process is pushed into the background. Y1 - 2019 SN - 1782-348X VL - 14 IS - 3 SP - 264 EP - 266 PB - Vrije Univ. CY - Bussels ER - TY - GEN A1 - Neubauer, Kai A1 - Haubelt, Christian A1 - Wanko, Philipp A1 - Schaub, Torsten H. T1 - Utilizing quad-trees for efficient design space exploration with partial assignment evaluation T2 - 2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC) N2 - Recently, it has been shown that constraint-based symbolic solving techniques offer an efficient way for deciding binding and routing options in order to obtain a feasible system level implementation. In combination with various background theories, a feasibility analysis of the resulting system may already be performed on partial solutions. That is, infeasible subsets of mapping and routing options can be pruned early in the decision process, which fastens the solving accordingly. However, allowing a proper design space exploration including multi-objective optimization also requires an efficient structure for storing and managing non-dominated solutions. In this work, we propose and study the usage of the Quad-Tree data structure in the context of partial assignment evaluation during system synthesis. Out experiments show that unnecessary dominance checks can be avoided, which indicates a preference of Quad-Trees over a commonly used list-based implementation for large combinatorial optimization problems. Y1 - 2018 SN - 978-1-5090-0602-1 U6 - https://doi.org/10.1109/ASPDAC.2018.8297362 SN - 2153-6961 SP - 434 EP - 439 PB - IEEE CY - New York ER - TY - GEN A1 - Bosser, Anne-Gwenn A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten H. T1 - Introducing temporal stable models for linear dynamic logic T2 - 16th International Conference on Principles of Knowledge Representation and Reasoning N2 - We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT. Y1 - 2018 UR - https://www.dc.fi.udc.es/~cabalar/del.pdf SP - 12 EP - 21 PB - ASSOC Association for the Advancement of Artificial Intelligence CY - Palo Alto ER - TY - GEN A1 - Cabalar, Pedro A1 - Fandinno, Jorge A1 - Schaub, Torsten H. A1 - Schellhorn, Sebastian T1 - Lower Bound Founded Logic of Here-and-There T2 - Logics in Artificial Intelligence N2 - A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz’ idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work. Y1 - 2019 SN - 978-3-030-19570-0 SN - 978-3-030-19569-4 U6 - https://doi.org/10.1007/978-3-030-19570-0_34 SN - 0302-9743 SN - 1611-3349 VL - 11468 SP - 509 EP - 525 PB - Springer CY - Cham ER - TY - GEN A1 - Fichte, Johannes Klaus A1 - Hecher, Markus A1 - Meier, Arne T1 - Counting Complexity for Reasoning in Abstract Argumentation T2 - The Thirty-Third AAAI Conference on Artificial Intelligence, the Thirty-First Innovative Applications of Artificial Intelligence Conference, the Ninth AAAI Symposium on Educational Advances in Artificial Intelligence N2 - In this paper, we consider counting and projected model counting of extensions in abstract argumentation for various semantics. When asking for projected counts we are interested in counting the number of extensions of a given argumentation framework while multiple extensions that are identical when restricted to the projected arguments count as only one projected extension. We establish classical complexity results and parameterized complexity results when the problems are parameterized by treewidth of the undirected argumentation graph. To obtain upper bounds for counting projected extensions, we introduce novel algorithms that exploit small treewidth of the undirected argumentation graph of the input instance by dynamic programming (DP). Our algorithms run in time double or triple exponential in the treewidth depending on the considered semantics. Finally, we take the exponential time hypothesis (ETH) into account and establish lower bounds of bounded treewidth algorithms for counting extensions and projected extension. Y1 - 2019 SN - 978-1-57735-809-1 SP - 2827 EP - 2834 PB - AAAI Press CY - Palo Alto ER - TY - GEN A1 - Sahlmann, Kristina A1 - Schwotzer, Thomas T1 - Ontology-based virtual IoT devices for edge computing T2 - Proceedings of the 8th International Conference on the Internet of Things N2 - An IoT network may consist of hundreds heterogeneous devices. Some of them may be constrained in terms of memory, power, processing and network capacity. Manual network and service management of IoT devices are challenging. We propose a usage of an ontology for the IoT device descriptions enabling automatic network management as well as service discovery and aggregation. Our IoT architecture approach ensures interoperability using existing standards, i.e. MQTT protocol and SemanticWeb technologies. We herein introduce virtual IoT devices and their semantic framework deployed at the edge of network. As a result, virtual devices are enabled to aggregate capabilities of IoT devices, derive new services by inference, delegate requests/responses and generate events. Furthermore, they can collect and pre-process sensor data. These tasks on the edge computing overcome the shortcomings of the cloud usage regarding siloization, network bandwidth, latency and speed. We validate our proposition by implementing a virtual device on a Raspberry Pi. KW - Internet of Things KW - Edge Computing KW - oneM2M Ontology KW - M2M KW - Semantic Interoperability KW - MQTT Y1 - 2018 SN - 978-1-4503-6564-2 U6 - https://doi.org/10.1145/3277593.3277597 SP - 1 EP - 7 PB - Association for Computing Machinery CY - New York ER - TY - GEN A1 - Böhne, Sebastian A1 - Kreitz, Christoph T1 - Learning how to prove BT - from the coq proof assistant to textbook style T2 - Electronic proceedings in theoretical computer science N2 - We have developed an alternative approach to teaching computer science students how to prove. First, students are taught how to prove theorems with the Coq proof assistant. In a second, more difficult, step students will transfer their acquired skills to the area of textbook proofs. In this article we present a realisation of the second step. Proofs in Coq have a high degree of formality while textbook proofs have only a medium one. Therefore our key idea is to reduce the degree of formality from the level of Coq to textbook proofs in several small steps. For that purpose we introduce three proof styles between Coq and textbook proofs, called line by line comments, weakened line by line comments, and structure faithful proofs. While this article is mostly conceptional we also report on experiences with putting our approach into practise. Y1 - 2018 U6 - https://doi.org/10.4204/EPTCS.267.1 SN - 2075-2180 IS - 267 SP - 1 EP - 18 PB - Open Publishing Association CY - Sydney ER - TY - GEN A1 - Giese, Holger ED - Kouchnarenko, Olga ED - Khosravi, Ramtin T1 - Formal models and analysis for self-adaptive cyber-physical systems BT - (extended abstract) T2 - Lecture notes in computer science N2 - In this extended abstract, we will analyze the current challenges for the envisioned Self-Adaptive CPS. In addition, we will outline our results to approach these challenges with SMARTSOS [10] a generic approach based on extensions of graph transformation systems employing open and adaptive collaborations and models at runtime for trustworthy self-adaptation, self-organization, and evolution of the individual systems and the system-of-systems level taking the independent development, operation, management, and evolution of these systems into account. Y1 - 2017 SN - 978-3-319-57666-4 SN - 978-3-319-57665-7 U6 - https://doi.org/10.1007/978-3-319-57666-4_1 SN - 0302-9743 SN - 1611-3349 VL - 10231 SP - 3 EP - 9 PB - Springer CY - Cham ER - TY - GEN A1 - Saint-Dizier, Patrick A1 - Stede, Manfred T1 - Foundations of the language of argumentation T2 - Argument & computation Y1 - 2017 U6 - https://doi.org/10.3233/AAC-170018 SN - 1946-2166 SN - 1946-2174 VL - 8 IS - 2 Special issue SP - 91 EP - 93 PB - IOS Press CY - Amsterdam ER - TY - GEN A1 - Fabian, Benjamin A1 - Baumann, Annika A1 - Ehlert, Mathias A1 - Ververis, Vasilis A1 - Ermakova, Tatiana T1 - CORIA - Analyzing internet connectivity risks using network graphs T2 - 2017 IEEE International Conference on Communications (ICC) N2 - The Internet can be considered as the most important infrastructure for modern society and businesses. A loss of Internet connectivity has strong negative financial impacts for businesses and economies. Therefore, assessing Internet connectivity, in particular beyond their own premises and area of direct control, is of growing importance in the face of potential failures, accidents, and malicious attacks. This paper presents CORIA, a software framework for an easy analysis of connectivity risks based on large network graphs. It provides researchers, risk analysts, network managers and security consultants with a tool to assess an organization's connectivity and paths options through the Internet backbone, including a user-friendly and insightful visual representation of results. CORIA is flexibly extensible in terms of novel data sets, graph metrics, and risk scores that enable further use cases. The performance of CORIA is evaluated by several experiments on the Internet graph and further randomly generated networks. KW - risk analysis KW - connectivity KW - graph analysis KW - complex networks KW - Internet Y1 - 2017 SN - 978-1-4673-8999-0 SN - 978-1-4673-9000-2 U6 - https://doi.org/10.1109/ICC.2017.7996828 SN - 1550-3607 PB - IEEE CY - Piscataway ER - TY - GEN A1 - Mühlbauer, Felix A1 - Schröder, Lukas A1 - Schölzel, Mario T1 - On hardware-based fault-handling in dynamically scheduled processors T2 - 20th International Symposium on Design and Diagnostics of Electronic Circuits & Systems (DDECS) 2017 N2 - This paper describes architectural extensions for a dynamically scheduled processor, so that it can be used in three different operation modes, ranging from high-performance, to high-reliability. With minor hardware-extensions of the control path, the resources of the superscalar data-path can be used either for high-performance execution, fail-safe-operation, or fault-tolerant-operation. This makes the processor-architecture a very good candidate for applications with dynamically changing reliability requirements, e.g. for automotive applications. The paper reports the hardware-overhead for the extensions, and investigates the performance penalties introduced by the fail-safe and fault-tolerant mode. Furthermore, a comprehensive fault simulation was carried out in order to investigate the fault-coverage of the proposed approach. Y1 - 2017 SN - 978-1-5386-0472-4 U6 - https://doi.org/10.1109/DDECS.2017.7934572 SN - 2334-3133 SN - 2473-2117 SP - 201 EP - 206 PB - IEEE CY - New York ER - TY - GEN A1 - Mühlbauer, Felix A1 - Schröder, Lukas A1 - Skoncej, Patryk A1 - Schölzel, Mario T1 - Handling manufacturing and aging faults with software-based techniques in tiny embedded systems T2 - 18th IEEE Latin American Test Symposium (LATS 2017) N2 - Non-volatile memory area occupies a large portion of the area of a chip in an embedded system. Such memories are prone to manufacturing faults, retention faults, and aging faults. The paper presents a single software based technique that allows for handling all of these fault types in tiny embedded systems without the need for hardware support. This is beneficial for low-cost embedded systems with simple memory architectures. A software infrastructure and a flow are presented that demonstrate how the presented technique is used in general for fault handling right after manufacturing and in-the-field. Moreover, a full implementation is presented for a MSP430 microcontroller, along with a discussion of the performance, overhead, and reliability impacts. Y1 - 2027 SN - 978-1-5386-0415-1 U6 - https://doi.org/10.1109/LATW.2017.7906756 PB - IEEE CY - New York ER -