Browsing IT Faculty / IT-fakulteten by Author "Piterman, Nir"

Now showing items 1-13 of 13

    • Actions over Core-closed Knowledge Bases 

      Cauli, Claudia; Ortiz, Magdalena; Piterman, Nir (2022)
      We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded ...

    • Fair Omega-regular Games 

      Hausmann, Daniel; Piterman, Nir; Saglam, Irmak; Schmuck, Anne-Kathrin (27th International Conference on Foundations of Software Science and Computation Structures, 2024)
      We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G=(V,E) and a set of fair moves E_f a subset of E a player is said ...

    • Games for Efficient Supervisor Synthesis 

      Hausmann, Daniel; Kumar Jha, Prabhat; Piterman, Nir (2023)
      In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one ...

    • Games for Efficient Supervisor Synthesis 

      Hausmann, Daniel; Prabhat, Kumar Jha; Piterman, Nir (2023)
      In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one ...

    • Incorporating Monitors in Reactive Synthesis without Paying the Price 

      Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo (19th International Symposium on Automated Technology for Verification and Analysis, 2021)
      Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative speci cations, and have found ...

    • Language Support for Verifying Reconfigurable Interacting Systems 

      Abd Alrahman, Yehia; Azzopardi, Shaun; Di Stefano, Luca; Piterman, Nir (2023)
      Reconfigurable interacting systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming ...

    • Model Checking Reconfigurable Interacting Systems 

      Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir (International Symposium on Leveraging Applications of Formal Methods, 2022)
      Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming ...

    • A PO Characterisation of Reconfiguration 

      Abd Alrahman, Yehia; Martel, Mauricio; Piterman, Nir (2022)
      We consider partial order semantics of concurrent systems in which local reconfigurations may have global side effects. That is, local changes happening to an entity may block or unblock events relating to others, namely, ...

    • ppLTLTT : Temporal Testing for Pure-Past Linear Temporal Logic Formulae 

      Azzopardi, Shaun; Lidell, David; Piterman, Nir; Schneider, Gerardo (2023)
      This paper presents ppLTLTT, a tool for translating pure-past linear temporal logic formulae into temporal testers in the form of automata. We show how ppLTLTT can be used to easily extend existing LTL-based tools, such ...

    • R-CHECK: A Model Checker for Verifying Reconfigurable MAS 

      Alrahman, Yehia Abd; Azzopardi, Shaun; Piterman, Nir (AAMAS 2022, 2022)
      Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by ...

    • Runtime Verification meets Controller Synthesis 

      Azzopardi, Shaun; Piterman, Nir; Schneider, Gerardo (2022)
      Reactive synthesis guarantees correct-by-construction controllers from logical specifications, but is costly—2EXPTIME-complete in the size of the specification. In a practical setting, the desired controllers need to ...

    • A Survey on Satisfiability Checking for the μ -Calculus Through Tree Automata 

      Hausmann, Daniel; Piterman, Nir (2022)
      Algorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and ...

    • Symbolic Solution of Emerson-Lei Games for Reactive Synthesis 

      Hausmann, Daniel; Lehaut, Mathieu; Piterman, Nir (2024)
      Emerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be ...