Clare Dixon (University of Manchester, UK)
TALK – Verifying Autonomous Robots: Challenges and Reflections
Autonomous robots such as robot assistants, healthcare robots, industrial robots, autonomous vehicles etc. are being developed to carry out a range of tasks in different environments. The robots need to be able to act autonomously, choosing between a range of activities. They may be operating close to or in collaboration with humans, or in environments hazardous to humans where the robot is hard to reach if it malfunctions. We need to ensure that such robots are reliable, safe and trustworthy. In this talk I will discuss experiences from several projects in developing and applying verification techniques to autonomous robotic systems. In particular we consider: a robot assistant in a domestic house, a robot co-worker for a cooperative manufacturing task, multiple robot systems and robots operating in hazardous environments.
BIO
Clare Dixon is Professor of Computer Science in the Department of Computer Science at the University of Manchester. She has recently moved to Manchester after almost twenty years as an academic in the Department of Computer Science at the University of Liverpool. Her research relates to the formal verification of systems and its application to areas such as autonomous systems, robotics, sensor systems, artificial intelligence and security. Recent research has focused on the verification of robot assistants, swarm robots and robotics in extreme environments. She also works on automated reasoning techniques for non-classical logics. She has been an investigator on twelve UKRI/EPSRC funded projects and her current projects include the Science of Sensor System Software, Future AI and Robotics Hub for Space (FAIR-SPACE), Robotics and Artificial Intelligence for Nuclear (RAIN). She is a member of the BSI Standards Committee, AMT/010 Robotics.
Pedro Cabalar (University of Corunna, Spain)
TALK – Temporal Modalities in Answer Set Programming
Based on the answer set (or stable model) semantics for logic programs, Answer Set Programming (ASP) has become one of the most successful paradigms for practical Knowledge Representation and problem solving. Although ASP is naturally equipped for solving static combinatorial problems up to NP complexity (or ΣP2 in the disjunctive case) its application to temporal scenarios has been frequent since its very beginning, partly due to its early use for reasoning about actions and change. Temporal problems normally suppose an extra challenge for ASP for several reasons. On the one hand, they normally raise the complexity (in the case of classical planning, for instance, it becomes PSPACE-complete), although this is usually accounted for by making repeated calls to an ASP solver. On the other hand, temporal scenarios also pose a representational challenge, since the basic ASP language does not support temporal expressions. To fill this representational gap, a temporal extension of ASP called Temporal Equilibrium Logic (TEL) was proposed in and extensively studied later. This formalism constitutes a modal, linear-time extension of Equilibrium Logic which, in its turn, is a complete logical characterisation of (standard) ASP based on the intermediate logic of Here-and-There (HT). As a result, TEL is an expressive non-monotonic modal logic that shares the syntax of Linear-Time Temporal Logic (LTL) but interprets temporal formulasunder a non-monotonic semantics that properly extends stable models.
BIO
Pedro Cabalar is an Associate Professor at the Computer Science Department, University of Corunna, Spain. He has published in relevant journals for Artificial Intelligence and Logic Programming like the prestigious Artificial Intelligence Journal (AIJ), the journal Theory and Practice on Logic Programming (TPLP), Annals of Mathematics and Artificial Intelligence (AMAI), AI Communications, the Journal of Applied Non-Classical Logics (JANCL) or the Logic Journal of the IGPL. He has regularly published in the main international conferences in the topic, like the International Joint Conference on Artificial Intelligence (IJCAI), the Intl. Conf. on Principles of Knowledge Representation and Reasoning (KR), the Conference on Artificial Intelligence (AAAI), the Intl. Conf. on Logic Programming (ICLP), the Intl. Conf. on Logic Programming and Nonmonotonic Reasoning (LPNMR), the European Conf. on Logics in Artificial Intelligence (JELIA), the European Conf. on Artificial Intelligence (ECAI), and some of their associated specialized workshops. He has co-chaired and organized the 12th edition of LPNMR in 2013 at A Coruña, and is also a frequent Program Committee member for conferences IJCAI, AAAI, KR, LPNMR, ICLP, ECAI and JELIA. He acts as reviewer for the AMS Mathematical Reviews of the American Mathematical Society. He has also acted as a reviewer in many journals in the area like the already mentioned TPLP, AIJ or the Journal of Artificial Intelligence Research, the Journal of Logic and Computation, the Journal of Applied Logic, the ACM Transactions on Computational Logic and others. He is involved in the European COST action “DigForASP: DIGital FORensics – evidence Analysis via intelligent Systems and Practices”, being the leader of Working Group 3, “Prototypes and Platforms.” In the past, he has served as area editor for the Association of Logic Programming Newsletter, he has been scientific editor of the Iberoamerican Journal on Artificial Intelligence and coordinated the PhD and MSc programmes of his Department. He has supervised two PhD theses.
Johann Eder (Alpen-Adria Universität Klagenfurt, Austria)
TALK – Time and Business Process Management: Problems, Achievements, Challenges
Processes have been successfully introduced for modeling dynamic phenomena in many areas like business, production, health care, etc. Many of these applications require to adequately deal with temporal aspects. Process models need to express temporal durations, temporal constraints like allowed time between events, and deadlines. For checking the correctness of process definitions with temporal constraints, different notions and algorithms have been developed. Schedules for the execution of processes can be computed and proactive time management supports process managers to avoid time failures during the execution of a process. We present an overview of the problems and the requirements for treating time in business processes and the solutions achieved by applying results and techniques of research in temporal representation and reasoning. We reflect where expectations have not yet been met and sketch challenges in temporal representation and reasoning for addressing advanced requirements of the management of business processes.
BIO
Johann Eder is full professor for Information and Communication Systems in the Department of Informatics-Systems of the Alpen-Adria Universität Klagenfurt, Austria. From 2005-2013 he served as Vice President of the Austrian Science Funds (FWF). He held positions at the Universities of Linz, Hamburg and Vienna and was visiting scholar at AT&T Shannon Labs, NJ, USA, the University of California Santa Barbara, CA, USA, and the New Jersey Institute of Technology, NJ, USA.The research interests of Johann Eder are information systems engineering, business process management, and data management for medical research. A particular focus of his work is the evolution of information systems and the modelling and management of temporal information and temporal constraints. Johann Eder successfully directed numerous competitively funded research projects on workflow management systems, temporal data warehousing, process modelling with temporal constraints, application interoperability and evolution, information systems modelling, information systems for medical research, etc. Johann Eder published more than 190 papers in peer reviewed international journals, conference proceedings, and edited books. He serves in the steering committees of CAiSE (chair), ADBIS, and TIME. He chaired resp. served in numerous program committees for international conferences and as editor and referee for international journals.