One way of modeling workflows in business process management (BPM) is by using a declarative approach, that is, instead of imperatively specifying what needs to be done, and in what order, one can specify constraints on what is allowed. The result is a more flexible model as everything that does not violate the specified constraints is allowed. In recent years, Linear Temporal Logic on finite traces (LTLf) has been one of the available logics used to specify such constraints. However, LTLf lacks the ability to monitor metaconstraints (i.e., constraints overconstraints). To handle this, one can use Linear Dynamic Logic on finite traces (LDLf) instead. In their paper Monitoring Constraints and Metaconstraints withTemporal Logics on Finite Traces, De Giacomo et al. (2020) presented a framework, and a formal way of translating LDLf formula to an executable Deterministic Finite Automaton (DFA), to be used in BPM. The algorithm they used for the translation was LDLf2NFA. This paper investigates if the construction time, and the size, of the DFA can be reduced by using a compositional algorithm, CLDLf, instead. The results show that the time can be reduced for larger formulae, that is, formulae with a length above 20. However, as both algorithms produce a minimal DFA as the end product, no reduction in size (i.e., the number of states) could be made.

Autonomous systems are slowly moving into the mainstream with things like self driving cars and autonomous robots in storage facilities already in use today. The aim of this project is to simulate a virtual bakery with a baker-robot (agent)that is able to complete recipes within strict deadlines.Signal temporal logic (STL) is used to define instructions that can be understood by the agent. In order to carry out these instructions, a control barrier function (CBF) is used.CBFs are time and state dependent, are used to describe the desired behavior of the agent, and are designer made. If the CBF corresponding to the task is non-negative from beginning to end during the task, the task has been completed successfully.A virtual robot was used in this project and was tasked with moving to and staying in different areas, which represents picking up and dropping off ingredients, all whilst staying within the boundaries of the bakery. The focus of this work is on completing the large amount (10+) of sequential tasks required to completea recipe. The CBF remained positive during the task, and the task was completed successfully. / Autonoma system börjar ta mer och mer plats i vardagen med saker som självkörande bilar och autonoma robotar i lagerlokaler som redan används idag. Syftet med det här projektet är att simulera ett virtuellt bageri med en bagarrobot (agent) som kan laga recept under strikta tidskrav. Signal temporal logic (STL) används för att definiera instruktioner som kan förstås av agenten. För att genomföra dessa instruktioner korrekt används en control barrier function (CBF). CBF:er är tidsoch tillståndsberoende, används för att beskriva agentens önskade beteende, och är skapade av en designer. Om CBF:en är positiv från början till slut under uppgiftens gång så har uppgiften genomförts som önskat. En virtuell robot användes i det här projektet och fick i uppdrag att flytta till och stanna inom olika områden, vilket representerar att plocka upp och lämna ingredienser, allt medan den vistas inom bageriets gränser. Fokus för detta arbete ligger på att slutföra den stora mängd (10+) av sekventiella uppgifter sim krävs för att laga ett recept. CBF:en var positiv under hela uppgiften, och uppgiften genomfördes framgångsrikt. / Kandidatexjobb i elektroteknik 2022, KTH, Stockholm

Formal methods play an important part in the development as well as testing stages of software and hardware systems. A significant and often overlooked part of the process is the development of specifications and correctness requirements for the system under test. Traditionally, English has been used as the specification language, which has resulted in verbose and difficult to use specification documents that are usually abandoned during product development. This research focuses on investigating the use of Live Sequence Charts (LSCs), a graphical and intuitive language directly suited for expressing communication behaviors of a system as the specification language for a system under test. The research presents two methods for using LSCs as a specification language: first, by translating LSCs to temporal logic, and second, by translating LSCs to an automaton structure that is directly suited for formal verification of systems. The research first presents the translation for each method and further, identifies the pros and cons for each verification method.

The world that we live in is a complex network of agents and their interactions which are termed as events. An instance of an event is composed of directly measurable low-level actions (which I term sub-events) having a temporal order. Also, the agents can act independently (e.g. voting) as well as collectively (e.g. scoring a touch-down in a football game) to perform an event. With the dawn of the new millennium, the low-level vision tasks such as segmentation, object classification, and tracking have become fairly robust. But a representational gap still exists between low-level measurements and high-level understanding of video sequences. This dissertation is an effort to bridge that gap where I propose novel learning, detection, representation, indexing and retrieval approaches for multi-agent events in videos. In order to achieve the goal of high-level understanding of videos, firstly, I apply statistical learning techniques to model the multiple agent events. For that purpose, I use the training videos to model the events by estimating the conditional dependencies between sub-events. Thus, given a video sequence, I track the people (heads and hand regions) and objects using a Meanshift tracker. An underlying rule-based system detects the sub-events using the tracked trajectories of the people and objects, based on their relative motion. Next, an event model is constructed by estimating the sub-event dependencies, that is, how frequently sub-event B occurs given that sub-event A has occurred. The advantages of such an event model are two-fold. First, I do not require prior knowledge of the number of agents involved in an event. Second, no assumptions are made about the length of an event. Secondly, after learning the event models, I detect events in a novel video by using graph clustering techniques. To that end, I construct a graph of temporally ordered sub-events occurring in the novel video. Next, using the learnt event model, I estimate a weight matrix of conditional dependencies between sub-events in the novel video. Further application of Normalized Cut (graph clustering technique) on the estimated weight matrix facilitate in detecting events in the novel video. The principal assumption made in this work is that the events are composed of highly correlated chains of sub-events that have high conditional dependency (association) within the cluster and relatively low conditional dependency (disassociation) between clusters. Thirdly, in order to represent the detected events, I propose an extension of CASE representation of natural languages. I extend CASE to allow the representation of temporal structure between sub-events. Also, in order to capture both multi-agent and multi-threaded events, I introduce a hierarchical CASE representation of events in terms of sub-events and case-lists. The essence of the proposition is that, based on the temporal relationships of the agent motions and a description of its state, it is possible to build a formal description of an event. Furthermore, I recognize the importance of representing the variations in the temporal order of sub-events, that may occur in an event, and encode the temporal probabilities directly into my event representation. The proposed extended representation with probabilistic temporal encoding is termed P-CASE that allows a plausible means of interface between users and the computer. Using the P-CASE representation I automatically encode the event ontology from training videos. This offers a significant advantage, since the domain experts do not have to go through the tedious task of determining the structure of events by browsing all the videos. Finally, I utilize the event representation for indexing and retrieval of events. Given the different instances of a particular event, I index the events using the P-CASE representation. Next, given a query in the P-CASE representation, event retrieval is performed using a two-level search. At the first level, a maximum likelihood estimate of the query event with the different indexed event models is computed. This provides the maximum matching event. At the second level, a matching score is obtained for all the event instances belonging to the maximum matched event model, using a weighted Jaccard similarity measure. Extensive experimentation was conducted for the detection, representation, indexing and retrieval of multiple agent events in videos of the meeting, surveillance, and railroad monitoring domains. To that end, the Semoran system was developed that takes in user inputs in any of the three forms for event retrieval: using predefined queries in P-CASE representation, using custom queries in P-CASE representation, or query by example video. The system then searches the entire database and returns the matched videos to the user. I used seven standard video datasets from the computer vision community as well as my own videos for testing the robustness of the proposed methods.

Most of the research on temporalized Description Logics (DLs) has concentrated on the case where temporal operators can occur within DL concept descriptions. In this setting, reasoning usually becomes quite hard if rigid roles, i.e., roles whose interpretation does not change over time, are available. In this paper, we consider the case where temporal operators are allowed to occur only in front of DL axioms (i.e., ABox assertions and general concept inclusion axioms), but not inside of concepts descriptions. As the temporal component, we use linear temporal logic (LTL) and in the DL component we consider the basic DL ALC. We show that reasoning in the presence of rigid roles becomes considerably simpler in this setting.

Often the addition of metric operators to qualitative temporal logics leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. The main result states that the language obtained by extending since/until logic of the real line with the operators 'sometime within n time units', n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.

We show how to combine the standard tableau system for the basic description logic ALC and Wolper´s tableau calculus for propositional temporal logic PTL (with the temporal operators ‘next-time’ and ‘until’) in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic PTL ALC of [19] interpreted in models with constant domains. We use the method of quasimodels [17, 15] to represent models with infinite domains, and the technique of minimal types [11] to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even do decidable fragments of first-order temporal logics.

The design and construction of interactive systems with high usability requires a user-centered approach to system development. In order to support such an approach, it is necessary to provide tools and representations reflecting a behavioral view of the interface—a view centered on user activities and the system activities and states perceived by the user. While behavioral representations exist, there is no behavioral model of interaction between a user and a system. Such a model is necessary for formalization and extension of existing behavioral representations. This dissertation presents a model of interactive behavior based on the timetree, a novel tree-based structure representing tasks, user actions, system activity, and system and interface state, all within a framework of branching sequential timelines. The model supports formal definitions, operations and abstraction techniques. Three application areas—a formal definition of an existing behavioral notation, connection between a behavioral representation and a formal model of input devices, and techniques for analysis of behavioral specifications—provide examples of the model's utility. / Ph. D.

We consider a number of temporal logics, some interval-based and some instant-based, and the choices that have to be made if we need to construct a computational framework for such a logic. We consider the axiomatisation of the accessibility relations of the underlying temporal structures when we are using a modal language as well as the formulation of axioms for distinguishing concepts like actions, events, processes and so on for systems using first-order languages. Finally, we briefly discuss the fields of application of temporal logics and list a number of fields that looks promising for further research. / Computer Science & Information Systems / M.Sc.(Computer Science)

Pushdown systems equip a finite state system with an unbounded stack memory, and are thus infinite state. By recording the call history on the stack, these systems provide a natural model for recursive procedure calls. Model-checking for pushdown systems has been well-studied. Tools implementing pushdown model-checking (e.g. Moped) are an essential back-end component of high-profile software model checkers such as SLAM, Blast and Terminator. Higher-order pushdown systems define a more complex memory structure: a higher-order stack is a stack of lower-order stacks. These systems form a robust hierarchy closely related to the Caucal hierarchy and higher-order recursion schemes. This latter connection demonstrates their importance as models for programs with higher-order functions. We study the global model-checking problem for (higher-order) pushdown systems. In particular, we present a new algorithm for computing the winning regions of a parity game played over an order-1 pushdown system. We then show how to compute the winning regions of two-player reachability games over order-n pushdown systems. These algorithms extend the saturation methods of Bouajjani, Esparza and Maler for order-1 pushdown systems, and Bouajjani and Meyer for higher-order pushdown systems with a single control state. These techniques begin with an automaton recognising (higher-order) stacks, and iteratively add new transitions until the automaton becomes saturated. The reachability result, presented at FoSSaCS 2007 and in the LMCS journal, is the main contribution of the thesis. We break the saturation paradigm by adding new states to the automaton during the iteration. We identify the fixed points required for termination by tracking the updates that are applied, rather than by observing the transition structure. We give a number of applications of this result to LTL model-checking, branching-time model-checking, non-emptiness of higher-order pushdown automata and Büchi games. Our second major contribution is the first application of the saturation technique to parity games. We begin with a mu-calculus characterisation of the winning region. This formula alternates greatest and least fixed point operators over a kind of reachability formula. Hence, we can use a version of our reachability algorithm, and modifications of the Büchi techniques, to compute the required result. The main advantages of this approach compared to existing techniques due to Cachat, Serre and Vardi et al. are that it is direct and that it is not immediately exponential in the number of control states, although the worst-case complexity remains the same.