@article(alur2002alternating,
 author       = {Rajeev Alur and Thomas A Henzinger and Orna Kupferman},
 year         = {2002},
 title        = {Alternating-time temporal logic},
 journal      = {Journal of the ACM (JACM)},
 volume       = {49},
 number       = {5},
 pages        = {672--713},
 doi          = {10.1145/585265.585270},
)
@inproceedings(alur1998mocha,
 author       = {Rajeev Alur and Thomas A Henzinger and Freddy YC Mang and Shaz Qadeer and Sriram K Rajamani and Serdar Tasiran},
 year         = {1998},
 title        = {MOCHA: Modularity in model checking},
 booktitle    = {CAV},
 organization = {Springer},
 pages        = {521--525},
 doi          = {10.1007/BFb0028774},
)
@article(bulling2022combining,
 author       = {Nils Bulling and Valentin Goranko},
 year         = {2022},
 title        = {Combining quantitative and qualitative reasoning in concurrent multi-player games},
 journal      = {Autonomous Agents and Multi-Agent Systems},
 volume       = {36},
 number       = {1},
 pages        = {1--33},
 doi          = {10.1007/s10458-021-09531-9},
)
@inproceedings(chang2010optimal,
 author       = {Fangzhe Chang and Jennifer Ren and Ramesh Viswanathan},
 year         = {2010},
 title        = {Optimal resource allocation in clouds},
 booktitle    = {2010 IEEE 3rd International Conference on Cloud Computing},
 organization = {IEEE},
 pages        = {418--425},
 doi          = {10.1109/CLOUD.2010.38},
)
@article(chatterjee2012energy,
 author       = {Krishnendu Chatterjee and Laurent Doyen},
 year         = {2012},
 title        = {Energy parity games},
 journal      = {Theoretical Computer Science},
 volume       = {458},
 pages        = {49--60},
 doi          = {10.1016/j.tcs.2012.07.038},
)
@inproceedings(chatterjee2005mean,
 author       = {Krishnendu Chatterjee and Thomas A Henzinger and Marcin Jurdzinski},
 year         = {2005},
 title        = {Mean-payoff parity games},
 booktitle    = {20th Annual IEEE Symposium on Logic in Computer Science (LICS'05)},
 organization = {IEEE},
 pages        = {178--187},
 doi          = {10.1109/LICS.2005.26},
)
@article(cimatti2000nusmv,
 author       = {Alessandro Cimatti and Edmund Clarke and Fausto Giunchiglia and Marco Roveri},
 year         = {2000},
 title        = {NuSMV: a new symbolic model checker},
 journal      = {STTT},
 volume       = {2},
 number       = {4},
 pages        = {410--425},
 doi          = {10.1007/s100090050046},
)
@inproceedings(de2018generalising,
 author       = {De Masellis, Riccardo and Valentin Goranko and Stefan Gruner and Nils Timm},
 year         = {2018},
 title        = {Generalising the Dining Philosophers problem: competitive dynamic resource allocation in multi-agent systems},
 booktitle    = {European Conference on Multi-Agent Systems},
 organization = {Springer},
 pages        = {30--47},
 doi          = {10.1007/978-3-030-14174-5_3},
)
@article(dimitrova2020reactive,
 author       = {Rayna Dimitrova and Mahsa Ghasemi and Ufuk Topcu},
 year         = {2020},
 title        = {Reactive synthesis with maximum realizability of linear temporal logic specifications},
 journal      = {Acta Informatica},
 volume       = {57},
 number       = {1},
 pages        = {107--135},
 doi          = {10.1007/s00236-019-00348-4},
)
@inproceedings(finkbeiner2018model,
 author       = {Bernd Finkbeiner and Christopher Hahn and Hazem Torfah},
 year         = {2018},
 title        = {Model checking quantitative hyperproperties},
 booktitle    = {International Conference on Computer Aided Verification},
 organization = {Springer},
 pages        = {144--163},
 doi          = {10.1007/978-3-319-96145-3_8},
)
@article(gutierrez2021equilibria,
 author       = {Julian Gutierrez and Aniello Murano and Giuseppe Perelli and Sasha Rubin and Thomas Steeples and Michael Wooldridge},
 year         = {2021},
 title        = {Equilibria for games with combined qualitative and quantitative objectives},
 journal      = {Acta Informatica},
 volume       = {58},
 number       = {6},
 pages        = {585--610},
 doi          = {10.1007/s00236-020-00385-4},
)
@article(gutierrez2017nash,
 author       = {Julian Gutierrez and Aniello Murano and Giuseppe Perelli and Sasha Rubin and Michael Wooldridge},
 year         = {2017},
 title        = {Nash equilibria in concurrent games with lexicographic preferences},
 doi          = {10.24963/ijcai.2017/148},
)
@article(hansen1990algorithms,
 author       = {Pierre Hansen and Brigitte Jaumard},
 year         = {1990},
 title        = {Algorithms for the maximum satisfiability problem},
 journal      = {Computing},
 volume       = {44},
 number       = {4},
 pages        = {279--303},
 doi          = {10.1007/BF02241270},
)
@article(kurose1989microeconomic,
 author       = {James F. Kurose and Rahul Simha},
 year         = {1989},
 title        = {A microeconomic approach to optimal resource allocation in distributed computer systems},
 journal      = {IEEE Transactions on computers},
 volume       = {38},
 number       = {5},
 pages        = {705--717},
 doi          = {10.1109/12.24272},
)
@phdthesis(2014maximum,
 author       = {Xiaojuan Liao},
 year         = {2014},
 title        = {Maximum Satisfiability Approach to Game Theory and Network Security},
 school       = {Kyushu University},
)
@article(lomuscio2017mcmas,
 author       = {Alessio Lomuscio and Hongyang Qu and Franco Raimondi},
 year         = {2017},
 title        = {MCMAS: an open-source model checker for the verification of multi-agent systems},
 journal      = {STTT},
 volume       = {19},
 number       = {1},
 pages        = {9--30},
 doi          = {10.1007/s10009-015-0378-x},
)
@article(martins2021open,
 author       = {Ruben Martins and Norbert Manthey and Terra-Neves, Miguel and Vasco Manquinho and In{\^e}s Lynce},
 year         = {2021},
 title        = {Open-WBO@ MaxSAT Evaluation 2020},
 journal      = {MaxSAT Evaluation 2020},
 pages        = {24},
)
@article(mukherjee2019adai,
 author       = {Amrit Mukherjee and Pratik Goswami and Ziwei Yan and Lixia Yang and Joel JPC Rodrigues},
 year         = {2019},
 title        = {ADAI and adaptive PSO-based resource allocation for wireless sensor networks},
 journal      = {IEEE Access},
 volume       = {7},
 pages        = {131163--131171},
 doi          = {10.1109/ACCESS.2019.2940821},
)
@article(nair2018multi,
 author       = {Arun Sukumaran Nair and Tareq Hossen and Mitch Campion and Daisy Flora Selvaraj and Neena Goveas and Naima Kaabouch and Prakash Ranganathan},
 year         = {2018},
 title        = {Multi-agent systems for resource allocation and scheduling in a smart grid},
 journal      = {Technology and Economics of Smart Grids and Sustainable Energy},
 volume       = {3},
 number       = {1},
 pages        = {1--15},
 doi          = {10.1007/s40866-018-0052-y},
)
@article(nash1950equilibrium,
 author       = {Nash Jr, John F},
 year         = {1950},
 title        = {Equilibrium points in n-person games},
 journal      = {Proceedings of the national academy of sciences},
 volume       = {36},
 number       = {1},
 pages        = {48--49},
 doi          = {10.1073/pnas.36.1.48},
)
@article(pilecki2017smc,
 author       = {Jerzy Pilecki and Marek A Bednarczyk and Wojciech Jamroga},
 year         = {2017},
 title        = {SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems},
 journal      = {Journal of Logic and Computation},
 volume       = {27},
 number       = {7},
 pages        = {1871--1895},
 doi          = {10.1093/logcom/exw032},
)
@inproceedings(schewe2008atl,
 author       = {Sven Schewe},
 year         = {2008},
 title        = {ATL* satisfiability is 2EXPTIME-complete},
 booktitle    = {International colloquium on automata, languages, and programming},
 organization = {Springer},
 pages        = {373--385},
 doi          = {10.1007/978-3-540-70583-3_31},
)
@inproceedings(timm2021model,
 author       = {Nils Timm and Josua Botha},
 year         = {2021},
 title        = {Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation},
 booktitle    = {Brazilian Symposium on Formal Methods},
 organization = {Springer},
 pages        = {53--69},
 doi          = {10.1007/978-3-030-92137-8_4},
)
@article(timm2020model,
 author       = {Nils Timm and Stefan Gruner and Madoda Nxumalo and Josua Botha},
 year         = {2020},
 title        = {Model checking safety and liveness via k-induction and witness refinement with constraint generation},
 journal      = {Science of Computer Programming},
 volume       = {200},
 pages        = {102532},
 doi          = {10.1016/j.scico.2020.102532},
)