Now showing items 18-23 of 23

    • 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 ...
    • 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 ...
    • Synchronous Agents, Verification, and Blame - A Deontic View 

      Kharraz, Karam; Azzopardi, Shaun; Schneider, Gerardo; Leucker, Martin (2023)
      A question we can ask of multi-agent systems is whether the agents’ collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, ...
    • Synthesis for prefix first-order logic on data words 

      Grange, J.; Lehaut, Mathieu (2024)
      We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications ...