Research Repository

See what's under the surface


Unbounded orchestrations of transdeucers for manufacturing (2019)
Conference Proceeding
Alechina, N., Brázdil, T., De Giacomo, G., Felli, P., Logan, B., & Vardi, M. Y. (2019). Unbounded orchestrations of transdeucers for manufacturing

There has recently been increasing interest in using reactive synthesis techniques to automate the production of manufacturing process plans. Previous work has assumed that the set of manufacturing resources is known and fixed in advance. In this pap... Read More

Qualitative spatial logic over 2D Euclidean spaces is not finitely axiomatisable (2018)
Conference Proceeding
Du, H., & Alechina, N. (in press). Qualitative spatial logic over 2D Euclidean spaces is not finitely axiomatisable. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI-19)

Several qualitative spatial logics used in reasoning about geospatial data have a sound and complete axiomatisation over metric spaces. It has been open whether the same ax-iomatisation is also sound and complete for 2D Euclidean spaces. We answer th... Read More

Model checking for Coalition Announcement Logic (2018)
Book Chapter
Galimullin, R., Alechina, N., & van Ditmarsch, H. (2018). Model checking for Coalition Announcement Logic. In F. Trollmann, & A. Turhan (Eds.), KI 2018: Advances in Artificial Intelligence, 41st German Conference on AI, Berlin, Germany, September 24–28, 2018, Proceedings, 11-23. Springer Publishing Company. doi:10.1007/978-3-030-00111-7_2

Coalition Announcement Logic (CAL) studies how a group of agents can enforce a certain outcome by making a joint announcement, regardless of any announcements made simultaneously by the opponents. The logic is useful to model imperfect information ga... Read More

Incentive-compatible mechanisms for norm monitoring in open multi-agent systems (Extended abstract) (2018)
Conference Proceeding
Alechina, N., Halpern, J. Y., Kash, I. A., & Logan, B. (2018). Incentive-compatible mechanisms for norm monitoring in open multi-agent systems (Extended abstract). In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligencedoi:10.24963/ijcai.2018/781

We consider the problem of detecting norm violations in open multi-agent systems (MAS). In this extended abstract, we outline the approach of [Alechina et al., 2018], and show how, using ideas from scrip systems, we can design mecha... Read More

Incentive-compatible mechanisms for norm monitoring in open multi-agent systems (2018)
Journal Article
Alechina, N., Halpern, J. Y., Kash, I. A., & Logan, B. (2018). Incentive-compatible mechanisms for norm monitoring in open multi-agent systems. Journal of Artificial Intelligence Research, 62, doi:10.1613/jair.1.11214. ISSN 1076-9757

We consider the problem of detecting norm violations in open multi-agent systems (MAS).We show how, using ideas from scrip systems, we can design mechanisms where the agents comprising the MAS are incentivised to monitor the actions of other agents f... Read More

On the complexity of resource-bounded logics (2018)
Journal Article
Alechina, N., Bulling, N., Demri, S., & Logan, B. S. (in press). On the complexity of resource-bounded logics. Theoretical Computer Science, doi:10.1016/j.tcs.2018.01.019

We revisit decidability results for resource-bounded logics and use decision problems on vector addition systems with states (VASS) in order to establish complexity characterisations of (decidable) model checking problems. We show that the model chec... Read More

Fair decomposition of group obligations (2017)
Journal Article
Alechina, N., Hoek, W. V. D., & Logan, B. (2017). Fair decomposition of group obligations. Journal of Logic and Computation, 27(7), doi:10.1093/logcom/exx012. ISSN 0955-792X

We consider the problem of decomposing a group norm into a set of individual obligations for the agents comprising the group, such that if the individual obligations are fulfilled, the group obligation is fulfilled. Such an assignment of tasks to age... Read More

The virtues of idleness: a decidable fragment of resource agent logic (2017)
Journal Article
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. N. (in press). The virtues of idleness: a decidable fragment of resource agent logic. Artificial Intelligence, doi:10.1016/j.artint.2016.12.005. ISSN 0004-3702

Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic (RAL), which extends ATL to allow the verification of properties of systems where agents act under resource constraints... Read More

On the complexity of resource-bounded logics (2016)
Conference Proceeding
Alechina, N., Bulling, N., Demri, S., & Logan, B. (2016). On the complexity of resource-bounded logics. In Reachability problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings, 36-50. doi:10.1007/978-3-319-45994-3_3

We revisit decidability results for resource-bounded logics and use decision problems for vector addition systems with states (VASS) to characterise the complexity of (decidable) model-checking problems. We show that the model-checking problem for th... Read More

Verifying systems of resource-bounded agents (2016)
Journal Article
Alechina, N., & Logan, B. (2016). Verifying systems of resource-bounded agents. Lecture Notes in Artificial Intelligence, 9709, doi:10.1007/978-3-319-40189-8_1. ISSN 0302-9743

Approaches to the verification of multi-agent systems are typically based on games or transition systems defined in terms of states and actions. However such approaches often ignore a key aspect of multi-agent systems, namely that the agents’ actions... Read More

A method for matching crowd-sourced and authoritative geospatial data (2016)
Journal Article
Du, H., Alechina, N., Jackson, M., & Hart, G. (2016). A method for matching crowd-sourced and authoritative geospatial data. Transactions in GIS, doi:10.1111/tgis.12210. ISSN 1361-1682

A method for matching crowd-sourced and authoritative geospatial data is presented. A level of tolerance is defined as an input parameter as some difference in the geometry representation of a spatial object is to be expected. The method generates ma... Read More

Coalition logic with individual, distributed and common knowledge (2016)
Journal Article
Ågotnes, T., & Alechina, N. (in press). Coalition logic with individual, distributed and common knowledge. Journal of Logic and Computation, doi:10.1093/logcom/exv085. ISSN 0955-792X

Coalition logic is currently one of the most popular logics for multi-agent systems. While logics combining coalitional and epistemic operators have received considerable attention, completeness results for epistemic extensions of coalition logic hav... Read More

On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic (2015)
Conference Proceeding
Alechina, N., Bulling, N., Logan, B., & Nguyen, H. N. (2015). On the boundary of (un)decidability: decidable model-checking for a fragment of resource agent logic

The model-checking problem for Resource Agent Logic is known to be undecidable. We review existing (un)decidability results and identify a significant fragment of the logic for which model checking is decidable. We discuss aspects which makes model c... Read More