@misc{NeubauerHaubeltWankoetal.2018, author = {Neubauer, Kai and Haubelt, Christian and Wanko, Philipp and Schaub, Torsten}, title = {Utilizing quad-trees for efficient design space exploration with partial assignment evaluation}, series = {2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC)}, journal = {2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5090-0602-1}, issn = {2153-6961}, doi = {10.1109/ASPDAC.2018.8297362}, pages = {434 -- 439}, year = {2018}, abstract = {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.}, language = {en} } @article{WahlHoelscher2018, author = {Wahl, Marina and H{\"o}lscher, Michael}, title = {Und am Wochenende Blended Learning}, series = {E-Learning Symposium 2018}, journal = {E-Learning Symposium 2018}, publisher = {Universit{\"a}tsverlag Potsdam}, address = {Potsdam}, doi = {10.25932/publishup-42191}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-421910}, pages = {17 -- 27}, year = {2018}, abstract = {Berufsbegleitende Studieng{\"a}nge stehen vor besonderen Schwierigkeiten, f{\"u}r die der Einsatz von Blended Learning-Szenarien sinnvoll sein kann. Welche speziellen Herausforderungen sich dabei ergeben und welche L{\"o}sungsans{\"a}tze dagegen steuern, betrachtet der folgende Artikel anhand eines Praxisberichts aus dem Studiengang M. P. A. Wissenschaftsmanagement an der Universit{\"a}t Speyer.}, language = {de} } @article{GianniniRichterServettoetal.2018, author = {Giannini, Paola and Richter, Tim and Servetto, Marco and Zucca, Elena}, title = {Tracing sharing in an imperative pure calculus}, series = {Science of computer programming}, volume = {172}, journal = {Science of computer programming}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0167-6423}, doi = {10.1016/j.scico.2018.11.007}, pages = {180 -- 202}, year = {2018}, abstract = {We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize, widely-used notions in literature, notably uniqueness and borrowing. Moreover, the calculus is pure in the sense that reduction is defined on language terms only, since they directly encode store. The advantage of this non-standard execution model with respect to a behaviorally equivalent standard model using a global auxiliary structure is that reachability relations among references are partly encoded by scoping. (C) 2018 Elsevier B.V. All rights reserved.}, language = {en} } @article{PrescherBornscheinKoehlmannetal.2018, author = {Prescher, Denise and Bornschein, Jens and K{\"o}hlmann, Wiebke and Weber, Gerhard}, title = {Touching graphical applications}, series = {Universal Access in the Information Society}, volume = {17}, journal = {Universal Access in the Information Society}, number = {2}, publisher = {Springer}, address = {Heidelberg}, issn = {1615-5289}, doi = {10.1007/s10209-017-0538-8}, pages = {391 -- 409}, year = {2018}, abstract = {Novel two-dimensional tactile displays enable blind users to not only get access to the textual but also to the graphical content of a graphical user interface. Due to the higher amount of information that can be presented in parallel, orientation and exploration can be more complex. In this paper we present the HyperBraille system, which consists of a pin-matrix device as well as a graphical screen reader providing the user with appropriate presentation and interaction possibilities. To allow for a detailed analysis of bimanual interaction strategies on a pin-matrix device, we conducted two user studies with a total of 12 blind people. The task was to fill in .pdf forms on the pin-matrix device by using different input methods, namely gestures, built-in hardware buttons as well as a conventional PC keyboard. The forms were presented in a semigraphic view type that not only contains Braille but also tactile widgets in a spatial arrangement. While completion time and error rate partly depended on the chosen input method, the usage of special reading strategies seemed to be independent of it. A direct comparison of the system and a conventional assistive technology (screen reader with single-line Braille device) showed that interaction on the pin-matrix device can be very efficient if the user is trained. The two-dimensional output can improve access to .pdf forms with insufficient accessibility as the mapping of input controls and the corresponding labels can be supported by a spatial presentation.}, language = {en} } @article{GebserKaminskiKaufmannetal.2018, author = {Gebser, Martin and Kaminski, Roland and Kaufmann, Benjamin and L{\"u}hne, Patrick and Obermeier, Philipp and Ostrowski, Max and Romero Davila, Javier and Schaub, Torsten and Schellhorn, Sebastian and Wanko, Philipp}, title = {The Potsdam Answer Set Solving Collection 5.0}, series = {K{\"u}nstliche Intelligenz}, volume = {32}, journal = {K{\"u}nstliche Intelligenz}, number = {2-3}, publisher = {Springer}, address = {Heidelberg}, issn = {0933-1875}, doi = {10.1007/s13218-018-0528-x}, pages = {181 -- 182}, year = {2018}, abstract = {The Potsdam answer set solving collection, or Potassco for short, bundles various tools implementing and/or applying answer set programming. The article at hand succeeds an earlier description of the Potassco project published in Gebser et al. (AI Commun 24(2):107-124, 2011). Hence, we concentrate in what follows on the major features of the most recent, fifth generation of the ASP system clingo and highlight some recent resulting application systems.}, language = {en} } @article{BanbaraInoueKaufmannetal.2018, author = {Banbara, Mutsunori and Inoue, Katsumi and Kaufmann, Benjamin and Okimoto, Tenda and Schaub, Torsten and Soh, Takehide and Tamura, Naoyuki and Wanko, Philipp}, title = {teaspoon}, series = {Annals of operation research}, volume = {275}, journal = {Annals of operation research}, number = {1}, publisher = {Springer}, address = {Dordrecht}, issn = {0254-5330}, doi = {10.1007/s10479-018-2757-7}, pages = {3 -- 37}, year = {2018}, abstract = {Answer Set Programming (ASP) is an approach to declarative problem solving, combining a rich yet simple modeling language with high performance solving capacities. We here develop an ASP-based approach to curriculum-based course timetabling (CB-CTT), one of the most widely studied course timetabling problems. The resulting teaspoon system reads a CB-CTT instance of a standard input format and converts it into a set of ASP facts. In turn, these facts are combined with a first-order encoding for CB-CTT solving, which can subsequently be solved by any off-the-shelf ASP systems. We establish the competitiveness of our approach by empirically contrasting it to the best known bounds obtained so far via dedicated implementations. Furthermore, we extend the teaspoon system to multi-objective course timetabling and consider minimal perturbation problems.}, language = {en} } @misc{SchaubWoltran2018, author = {Schaub, Torsten and Woltran, Stefan}, title = {Special issue on answer set programming}, series = {K{\"u}nstliche Intelligenz}, volume = {32}, journal = {K{\"u}nstliche Intelligenz}, number = {2-3}, publisher = {Springer}, address = {Heidelberg}, issn = {0933-1875}, doi = {10.1007/s13218-018-0554-8}, pages = {101 -- 103}, year = {2018}, language = {en} } @article{BordihnMitranaNegruetal.2018, author = {Bordihn, Henning and Mitrana, Victor and Negru, Maria C. and Paun, Andrei and Paun, Mihaela}, title = {Small networks of polarized splicing processors are universal}, series = {Natural computing : an innovative journal bridging biosciences and computer sciences ; an international journal}, volume = {17}, journal = {Natural computing : an innovative journal bridging biosciences and computer sciences ; an international journal}, number = {4}, publisher = {Springer}, address = {Dordrecht}, issn = {1567-7818}, doi = {10.1007/s11047-018-9691-0}, pages = {799 -- 809}, year = {2018}, abstract = {In this paper, we consider the computational power of a new variant of networks of splicing processors in which each processor as well as the data navigating throughout the network are now considered to be polarized. While the polarization of every processor is predefined (negative, neutral, positive), the polarization of data is dynamically computed by means of a valuation mapping. Consequently, the protocol of communication is naturally defined by means of this polarization. We show that networks of polarized splicing processors (NPSP) of size 2 are computationally complete, which immediately settles the question of designing computationally complete NPSPs of minimal size. With two more nodes we can simulate every nondeterministic Turing machine without increasing the time complexity. Particularly, we prove that NPSP of size 4 can accept all languages in NP in polynomial time. Furthermore, another computational model that is universal, namely the 2-tag system, can be simulated by NPSP of size 3 preserving the time complexity. All these results can be obtained with NPSPs with valuations in the set as well. We finally show that Turing machines can simulate a variant of NPSPs and discuss the time complexity of this simulation.}, language = {en} } @misc{MarweckiBaudisch2018, author = {Marwecki, Sebastian and Baudisch, Patrick}, title = {Scenograph}, series = {UIST '18: Proceedings of the 31st Annual ACM Symposium on User Interface Software and Technology}, journal = {UIST '18: Proceedings of the 31st Annual ACM Symposium on User Interface Software and Technology}, publisher = {Association for Computing Machinery}, address = {New York}, isbn = {978-1-4503-5948-1}, doi = {10.1145/3242587.3242648}, pages = {511 -- 520}, year = {2018}, abstract = {When developing a real-walking virtual reality experience, designers generally create virtual locations to fit a specific tracking volume. Unfortunately, this prevents the resulting experience from running on a smaller or differently shaped tracking volume. To address this, we present a software system called Scenograph. The core of Scenograph is a tracking volume-independent representation of real-walking experiences. Scenograph instantiates the experience to a tracking volume of given size and shape by splitting the locations into smaller ones while maintaining narrative structure. In our user study, participants' ratings of realism decreased significantly when existing techniques were used to map a 25m2 experience to 9m2 and an L-shaped 8m2 tracking volume. In contrast, ratings did not differ when Scenograph was used to instantiate the experience.}, language = {en} } @article{GebserObermeierSchaubetal.2018, author = {Gebser, Martin and Obermeier, Philipp and Schaub, Torsten and Ratsch-Heitmann, Michel and Runge, Mario}, title = {Routing driverless transport vehicles in car assembly with answer set programming}, series = {Theory and practice of logic programming}, volume = {18}, journal = {Theory and practice of logic programming}, number = {3-4}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068418000182}, pages = {520 -- 534}, year = {2018}, abstract = {Automated storage and retrieval systems are principal components of modern production and warehouse facilities. In particular, automated guided vehicles nowadays substitute human-operated pallet trucks in transporting production materials between storage locations and assembly stations. While low-level control systems take care of navigating such driverless vehicles along programmed routes and avoid collisions even under unforeseen circumstances, in the common case of multiple vehicles sharing the same operation area, the problem remains how to set up routes such that a collection of transport tasks is accomplished most effectively. We address this prevalent problem in the context of car assembly at Mercedes-Benz Ludwigsfelde GmbH, a large-scale producer of commercial vehicles, where routes for automated guided vehicles used in the production process have traditionally been hand-coded by human engineers. Such adhoc methods may suffice as long as a running production process remains in place, while any change in the factory layout or production targets necessitates tedious manual reconfiguration, not to mention the missing portability between different production plants. Unlike this, we propose a declarative approach based on Answer Set Programming to optimize the routes taken by automated guided vehicles for accomplishing transport tasks. The advantages include a transparent and executable problem formalization, provable optimality of routes relative to objective criteria, as well as elaboration tolerance towards particular factory layouts and production targets. Moreover, we demonstrate that our approach is efficient enough to deal with the transport tasks evolving in realistic production processes at the car factory of Mercedes-Benz Ludwigsfelde GmbH.}, language = {en} } @misc{KrstićJentzsch2018, author = {Krstić, Miloš and Jentzsch, Anne-Kristin}, title = {Reliability, safety and security of the electronics in automated driving vehicles - joint lab lecturing approach}, series = {2018 12TH European Workshop on Microelectronics Education (EWME)}, journal = {2018 12TH European Workshop on Microelectronics Education (EWME)}, publisher = {IEEE}, address = {New York}, isbn = {978-1-5386-1157-9}, pages = {21 -- 22}, year = {2018}, abstract = {This paper proposes an education approach for master and bachelor students to enhance their skills in the area of reliability, safety and security of the electronic components in automated driving. The approach is based on the active synergetic work of research institutes, academia and industry in the frame of joint lab. As an example, the jointly organized summer school with the respective focus is organized and elaborated.}, language = {en} } @incollection{KiyKnothMueller2018, author = {Kiy, Alexander and Knoth, Alexander Henning and M{\"u}ller, Ina}, title = {ReflectUP-App Situative und kontextbezogene Evaluation des Studieneinstiegs}, series = {Digitalisierung der Hochschullehre Neue Anforderungen an die Evaluation?}, booktitle = {Digitalisierung der Hochschullehre Neue Anforderungen an die Evaluation?}, editor = {Harris-Huemmert, Susan and Pohlenz, Philipp and Mitterauer, Lukas}, publisher = {Waxmann}, address = {M{\"u}nster}, isbn = {978-3-8309-3807-1}, publisher = {Universit{\"a}t Potsdam}, pages = {85 -- 102}, year = {2018}, language = {de} } @misc{BordihnNagyVaszil2018, author = {Bordihn, Henning and Nagy, Benedek and Vaszil, Gy{\"o}rgy}, title = {Preface: Non-classical models of automata and applications VIII}, series = {RAIRO-Theoretical informatics and appli and applications}, volume = {52}, journal = {RAIRO-Theoretical informatics and appli and applications}, number = {2-4}, publisher = {EDP Sciences}, address = {Les Ulis}, issn = {0988-3754}, doi = {10.1051/ita/2018019}, pages = {87 -- 88}, year = {2018}, language = {en} } @misc{SahlmannSchwotzer2018, author = {Sahlmann, Kristina and Schwotzer, Thomas}, title = {Ontology-based virtual IoT devices for edge computing}, series = {Proceedings of the 8th International Conference on the Internet of Things}, journal = {Proceedings of the 8th International Conference on the Internet of Things}, publisher = {Association for Computing Machinery}, address = {New York}, isbn = {978-1-4503-6564-2}, doi = {10.1145/3277593.3277597}, pages = {1 -- 7}, year = {2018}, abstract = {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.}, language = {en} } @phdthesis{Ostrowski2018, author = {Ostrowski, Max}, title = {Modern constraint answer set solving}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-407799}, school = {Universit{\"a}t Potsdam}, pages = {135}, year = {2018}, abstract = {Answer Set Programming (ASP) is a declarative problem solving approach, combining a rich yet simple modeling language with high-performance solving capabilities. Although this has already resulted in various applications, certain aspects of such applications are more naturally modeled using variables over finite domains, for accounting for resources, fine timings, coordinates, or functions. Our goal is thus to extend ASP with constraints over integers while preserving its declarative nature. This allows for fast prototyping and elaboration tolerant problem descriptions of resource related applications. The resulting paradigm is called Constraint Answer Set Programming (CASP). We present three different approaches for solving CASP problems. The first one, a lazy, modular approach combines an ASP solver with an external system for handling constraints. This approach has the advantage that two state of the art technologies work hand in hand to solve the problem, each concentrating on its part of the problem. The drawback is that inter-constraint dependencies cannot be communicated back to the ASP solver, impeding its learning algorithm. The second approach translates all constraints to ASP. Using the appropriate encoding techniques, this results in a very fast, monolithic system. Unfortunately, due to the large, explicit representation of constraints and variables, translation techniques are restricted to small and mid-sized domains. The third approach merges the lazy and the translational approach, combining the strength of both while removing their weaknesses. To this end, we enhance the dedicated learning techniques of an ASP solver with the inferences of the translating approach in a lazy way. That is, the important knowledge is only made explicit when needed. By using state of the art techniques from neighboring fields, we provide ways to tackle real world, industrial size problems. By extending CASP to reactive solving, we open up new application areas such as online planning with continuous domains and durations.}, language = {en} } @article{LiChenNofaletal.2018, author = {Li, Yuanqing and Chen, Li and Nofal, Issam and Chen, Mo and Wang, Haibin and Liu, Rui and Chen, Qingyu and Krstić, Miloš and Shi, Shuting and Guo, Gang and Baeg, Sang H. and Wen, Shi-Jie and Wong, Richard}, title = {Modeling and analysis of single-event transient sensitivity of a 65 nm clock tree}, series = {Microelectronics reliability}, volume = {87}, journal = {Microelectronics reliability}, publisher = {Elsevier}, address = {Oxford}, issn = {0026-2714}, doi = {10.1016/j.microrel.2018.05.016}, pages = {24 -- 32}, year = {2018}, abstract = {The soft error rate (SER) due to heavy-ion irradiation of a clock tree is investigated in this paper. A method for clock tree SER prediction is developed, which employs a dedicated soft error analysis tool to characterize the single-event transient (SET) sensitivities of clock inverters and other commercial tools to calculate the SER through fault-injection simulations. A test circuit including a flip-flop chain and clock tree in a 65 nm CMOS technology is developed through the automatic ASIC design flow. This circuit is analyzed with the developed method to calculate its clock tree SER. In addition, this circuit is implemented in a 65 nm test chip and irradiated by heavy ions to measure its SER resulting from the SETs in the clock tree. The experimental and calculation results of this case study present good correlation, which verifies the effectiveness of the developed method.}, language = {en} } @incollection{KiyLucke2018, author = {Kiy, Alexander and Lucke, Ulrike}, title = {Mobile Unterst{\"u}tzung im Studienalltag zwischen Generalit{\"a}t und Individualit{\"a}t}, series = {Handbuch Mobile Learning}, volume = {2018}, booktitle = {Handbuch Mobile Learning}, editor = {de Witt, Claudia and Gloerfeld, Christina}, publisher = {Springer VS}, address = {Wiesbaden}, isbn = {978-3-658-19123-8}, doi = {10.1007/978-3-658-19123-8_37}, publisher = {Universit{\"a}t Potsdam}, pages = {777 -- 808}, year = {2018}, abstract = {Mobile Endger{\"a}te und Applikationen (Apps) sind dank vielf{\"a}ltiger Kommunikations-, Informations- und Assistenzfunktionen zu einem unverzichtbaren Bestandteil unseres t{\"a}glichen Lebens geworden. Inzwischen hat sich insbesondere im Hochschulumfeld eine bunte Vielfalt an mobilen Unterst{\"u}tzungsangeboten etabliert, beginnend bei zentral angebotenen Uni-Apps bis hin zu unterschiedlichen Apps zur Ausgestaltung einzelner Lehrveranstaltungen oder individueller Lehr- und Lernszenarien. Angesichts der großen Aufw{\"a}nde zur Entwicklung, Distribution und Pflege mobiler Anwendungen ist ein Einsatz f{\"u}r eine m{\"o}glichst große Zielgruppe w{\"u}nschenswert. Dies kann jedoch mit dem Charakter mobiler Endger{\"a}te als pers{\"o}nliche, individualisierte Assistenten kollidieren. In diesem Beitrag werden entlang dieses Spektrums zwischen (fach-)spezifischen Einzell{\"o}sungen und breiten Allroundern verschiedene mobile Unterst{\"u}tzungsangebote aus dem Hochschulbereich vorgestellt, hinsichtlich ihres Einsatzes kontextuell eingeordnet und systematisiert. Dies umfasst mobile Anwendungen, die allgemeine organisatorische Aspekte des Studiums, bestimmte Felder wie die Studieneingangsphase oder die konkrete Begleitung hybrider Lernszenarien fokussieren. Es schließt sich eine App-Auswahl an, die fachspezifischen Aspekten Rechnung tr{\"a}gt und in denen Inhalte in Form von Serious Games, Simulationen und Inhaltsmodulen aufbereitet sind. Neben Lehre und Studium wird auch die Forschung in den Fokus ger{\"u}ckt, wo Apps gleichermaßen als Forschungsgegenstand und Datenerhebungsinstrument wirken. Aus der F{\"u}lle dieser Entwicklungen resultiert eine App-Vielfalt, die verschiedene Herausforderungen aufwirft. Der Beitrag stellt die spezifischen Herausforderungen zusammen und spricht Empfehlungen aus. Dabei werden sowohl organisatorische, inhaltliche und technische Fragestellungen thematisiert als auch rechtliche Gesichtspunkte bez{\"u}glich Datenschutz und Copyright tangiert.}, language = {de} } @article{BaierDiCiccioMendlingetal.2018, author = {Baier, Thomas and Di Ciccio, Claudio and Mendling, Jan and Weske, Mathias}, title = {Matching events and activities by integrating behavioral aspects and label analysis}, series = {Software and systems modeling}, volume = {17}, journal = {Software and systems modeling}, number = {2}, publisher = {Springer}, address = {Heidelberg}, issn = {1619-1366}, doi = {10.1007/s10270-017-0603-z}, pages = {573 -- 598}, year = {2018}, abstract = {Nowadays, business processes are increasingly supported by IT services that produce massive amounts of event data during the execution of a process. These event data can be used to analyze the process using process mining techniques to discover the real process, measure conformance to a given process model, or to enhance existing models with performance information. Mapping the produced events to activities of a given process model is essential for conformance checking, annotation and understanding of process mining results. In order to accomplish this mapping with low manual effort, we developed a semi-automatic approach that maps events to activities using insights from behavioral analysis and label analysis. The approach extracts Declare constraints from both the log and the model to build matching constraints to efficiently reduce the number of possible mappings. These mappings are further reduced using techniques from natural language processing, which allow for a matching based on labels and external knowledge sources. The evaluation with synthetic and real-life data demonstrates the effectiveness of the approach and its robustness toward non-conforming execution logs.}, language = {en} } @misc{BoehneKreitz2018, author = {B{\"o}hne, Sebastian and Kreitz, Christoph}, title = {Learning how to prove}, series = {Electronic proceedings in theoretical computer science}, journal = {Electronic proceedings in theoretical computer science}, number = {267}, publisher = {Open Publishing Association}, address = {Sydney}, issn = {2075-2180}, doi = {10.4204/EPTCS.267.1}, pages = {1 -- 18}, year = {2018}, abstract = {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.}, language = {en} } @misc{BosserCabalarDieguezetal.2018, author = {Bosser, Anne-Gwenn and Cabalar, Pedro and Dieguez, Martin and Schaub, Torsten}, title = {Introducing temporal stable models for linear dynamic logic}, series = {16th International Conference on Principles of Knowledge Representation and Reasoning}, journal = {16th International Conference on Principles of Knowledge Representation and Reasoning}, publisher = {ASSOC Association for the Advancement of Artificial Intelligence}, address = {Palo Alto}, pages = {12 -- 21}, year = {2018}, abstract = {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.}, language = {en} }