To build a theory of intention revision for agents operating in stochastic environments, we need a logic in which we can explicitly reason about their decision-making policies and those policiesâ€™ uncertain outcomes. Toward this end, we propose PLBP, a novel probabilistic temporal logic for Markov Decision Processes that allows us to reason about policies of bounded size. The logic is designed so that its expressive power is sufficient for the intended applications, whilst at the same time possessing strong computational properties. We prove that the satisfiability problem for our logic is decidable, and that its model checking problem is PSPACE-complete. This allows us to e.g. algorithmically verify whether an agentâ€™s intentions are coherent, or whether a specific policy satisfies safety and/or liveness properties.

We put forward a formal model of participatory budgeting where projects can incur costs with respect to several different resources, such as money, energy, or emission allowances. We generalise several well-known mechanisms from the usual single-resource setting to this multi-resource setting and analyse their algorithmic efficiency, the extent to which they are immune to strategic manipulation, and the degree of proportional representation they can guarantee. We also prove a general impossibility theorem establishing the incompatibility of proportionality and strategyproofness for this model.

abstracts & short contributions

2023

AAAI-SSS

Probabilistic Temporal Logic for Reasoning about Bounded Policies

To build a theory of intention revision for agents operating in stochastic environments, we need a logic in which we can explicitly reason about their decision-making policies and those policiesâ€™ uncertain outcomes. Towards this end, we propose PLBP, a novel probabilistic temporal logic for Markov Decision Processes that allows us to reason about finite traces and policies of bounded size. The logic is designed so that its expressive power is sufficient for the intended applications, whilst at the same time possessing strong computational properties. We prove that the satisfiability problem for our logic is decidable, and that its model checking problem is PSPACE-complete. This allows us to e.g. algorithmically verify whether an agentsâ€™ intentions are coherent, or whether a specific policy satisfies safety and/or liveness properties.

2022

LAMAS & SR

A Probabilistic Finite Temporal Logic for Policies and Intentions

We propose a new probabilistic temporal logic for Markov decision processes allowing us to reason about finite histories and policies. We comment on how the logic can express statements important for a theory of intention revision, show that it possesses the finite model property, and show that the model checking and satisfiability problems for the logic are both decidable.

We study coalgebraic generalisations of Fittingâ€™s multiagent semantics of modal logic from his article "How True It Is = Who Says Itâ€™s True". First, we lift two-valued logics via distributive laws to multiagent logics on (co-)Kleisli categories, thus giving a category-theoretic account of Fittingâ€™s notion of slicing. Second, we provide an alternative semantics where slicing is modelled in the functor instead of in the base category. Third, we extend our models to work with ordered sets of agents, and show that this enables the modelling of differences in expertise, certainty, and ability to achieve outcomes.

theses

2021

Multivalued Coalgebraic Modal Logic for Multiagent Systems and Multiplayer Games

This thesis investigates coalgebraic generalizations of two multiagent modal logics from the literature, in which truth values are identified with sets of agents. In the first logic, which is due to Melvin Fitting, the truth value of a formula is identified as the set of agents for whom the formula is true, while in the second logic, which is due to Loes Olde Loohuis and Yde Venema, the truth value of a formula is identified as the set of players that have a winning strategy at a corresponding position in a multiplayer evaluation game. For the first logic, we identify a new base category of interest, from which the generalization comes forth naturally using the theory of coalgebraic modal logic, and give proofs of adequacy and expressivity. For the second logic, we define multiplayer evaluation games in which play proceeds nondeterministically, and use the well-known fact that predicate liftings induce transformations from coalgebras to neighbourhood frames. Finally, we prove that fragments of our generalizations are equiexpressive, and show how they can naturally describe situations with multiple agents.

2018

A Performance Analysis of Filtering Methods Applied to WiFi-Based Position Reconstruction

WiFi-based position reconstruction is becoming an increasingly important field of study, with applications in both ubiquitous computing and crowd analysis. Many approaches to this problem provide high accuracy at the cost of low ease of use, by often requiring either specialised hardware or costly offline phases. We compare and analyze the use of several filtering methods in order to increase the accuracy of a low-cost and out-of-the-box trilateration approach to WiFi-based position reconstruction, by applying the filtering methods to positions reconstructed from walks through the largest stadium in the Netherlands. The compared filtering methods consist of exponential filtering, Gaussian filters, Savitzky-Golay filters, median filters and Kalman filters, along with several variations. In addition to the performance comparison, we apply sensitivity analysis to the parameters of the methods, determining which are of most importance to resulting accuracy. We find that the median filter and some of its variations perform the best, improving upon the baseline accuracy by seven metres. Other high performers include the Gaussian and Savitzky-Golay filters, which like the median filter, are simple in their procedures and require few parameters.