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.
@inproceedings{MotamedEtAl2023Probabilistic,author={Motamed, Nima and Alechina, Natasha and Dastani, Mehdi and Doder, Dragan and Logan, Brian},title={Probabilistic Temporal Logic for Reasoning about Bounded Policies},year={2023},month=aug,booktitle={Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI-23)},editor={Elkind, Edith},pages={3296--3303},note={Main Track},doi={10.24963/ijcai.2023/367},}
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.
@inproceedings{MotamedEtAl2022Participatory,author={Motamed, Nima and Soeteman, Arie and Rey, Simon and Endriss, Ulle},title={Participatory Budgeting with Multiple Resources},year={2022},month=sep,booktitle={Proceedings of the 19th European Conference on Multi-Agent Systems (EUMAS 2022)},pages={330--347},doi={10.1007/978-3-031-20614-6_19},editors={Rothe, Jörg and Baumeister, Dorothea},publisher={Springer},}
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.
@inproceedings{MotamedEtAl2023Probabilistic,author={Motamed, Nima and Alechina, Natasha and Dastani, Mehdi and Doder, Dragan and Logan, Brian},title={Probabilistic Temporal Logic for Reasoning about Bounded Policies},year={2023},month=mar,booktitle={AAAI 2023 Spring Symposium On the Effectiveness of Temporal Logics on Finite Traces in AI},editors={Bansal, Suguman and Di Stasio, Antonio and Rubin, Sasha and Zhu, Shufang},}
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.
@inproceedings{MotamedEtAl2022Probabilistic,author={Motamed, Nima and Alechina, Natasha and Dastani, Mehdi and Doder, Dragan},title={A Probabilistic Finite Temporal Logic for Policies and Intentions},year={2022},month=aug,booktitle={International Workshop on Logical Aspects in Multi-Agent Systems and Strategic Reasoning 2022 (LAMAS & SR 2022)},editors={Mogavero, Fabio, and Pinchinat, Sophie},}
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.
@inproceedings{KurzMotamed2022Boolean,author={Kurz, Alexander and Motamed, Nima},title={Boolean-Valued Multiagent Coalgebraic Logic},year={2022},month=apr,booktitle={Short Contributions of the 16th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022)},editors={Hansen, Helle Hvid and Zanasi, Fabio},}
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.
@phdthesis{Motamed2021Thesis,author={Motamed, Nima},title={Multivalued Coalgebraic Modal Logic for Multiagent Systems and Multiplayer Games},school={Institute for Logic, Language and Computation, University of Amsterdam},year={2021},month=aug,address={Amsterdam, The Netherlands},type={Master's thesis},}
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.
@phdthesis{Motamed2018Thesis,author={Motamed, Nima},title={A Performance Analysis of Filtering Methods Applied to WiFi-Based Position Reconstruction},school={University of Amsterdam},year={2018},month=aug,address={Amsterdam, The Netherlands},type={Bachelor's thesis},}