Verifying requirements for resource-bounded agents
This thesis presents frameworks for the modelling and verification of resource-bounded reasoning agents. The resources considered include the time, memory, and communication bandwidth required by agents to achieve a goal. The scalability and expressiveness of standard model checking techniques is in...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2011
|
| Online Access: | https://eprints.nottingham.ac.uk/12057/ |
| _version_ | 1848791421261185024 |
|---|---|
| author | Abdur, Rakib |
| author_facet | Abdur, Rakib |
| author_sort | Abdur, Rakib |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | This thesis presents frameworks for the modelling and verification of resource-bounded reasoning agents. The resources considered include the time, memory, and communication bandwidth required by agents to achieve a goal. The scalability and expressiveness of standard model checking techniques is investigated using two typical multiagent reasoning problems which can be easily parameterised to increase or decrease the problem size. Both a complexity analysis and experimental results suggest that reasonably sized problem instances are unlikely to be tractable for a standard model checker without steps to reduce the branching factor of the state space. We propose two approaches to address this problem: the use of abstract specifications to model the behaviour of some of the agents in the system, and exploiting information about the reasoning strategy adopted by the agents. Abstract specifications are given as Linear Temporal Logic (LTL) formulae which describe the external behaviour of the agents, allowing their temporal behaviour to be compactly modelled. Conversely, reasoning strategies allow the detailed specification of the ordering of steps in the agent’s reasoning process. Both approaches have been combined in an automated verification tool TVRBA for rule-based multi-agent systems which allows the designer to specify information about agents’ interaction, behaviour, and execution strategy at different levels of abstraction. The TVRBA tool generates an encoding of the system for the Maude LTL model checker, allowing properties of the system to be verified. The scalability of the new approach is illustrated using three case studies. |
| first_indexed | 2025-11-14T18:28:14Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-12057 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:28:14Z |
| publishDate | 2011 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-120572025-02-28T11:17:15Z https://eprints.nottingham.ac.uk/12057/ Verifying requirements for resource-bounded agents Abdur, Rakib This thesis presents frameworks for the modelling and verification of resource-bounded reasoning agents. The resources considered include the time, memory, and communication bandwidth required by agents to achieve a goal. The scalability and expressiveness of standard model checking techniques is investigated using two typical multiagent reasoning problems which can be easily parameterised to increase or decrease the problem size. Both a complexity analysis and experimental results suggest that reasonably sized problem instances are unlikely to be tractable for a standard model checker without steps to reduce the branching factor of the state space. We propose two approaches to address this problem: the use of abstract specifications to model the behaviour of some of the agents in the system, and exploiting information about the reasoning strategy adopted by the agents. Abstract specifications are given as Linear Temporal Logic (LTL) formulae which describe the external behaviour of the agents, allowing their temporal behaviour to be compactly modelled. Conversely, reasoning strategies allow the detailed specification of the ordering of steps in the agent’s reasoning process. Both approaches have been combined in an automated verification tool TVRBA for rule-based multi-agent systems which allows the designer to specify information about agents’ interaction, behaviour, and execution strategy at different levels of abstraction. The TVRBA tool generates an encoding of the system for the Maude LTL model checker, allowing properties of the system to be verified. The scalability of the new approach is illustrated using three case studies. 2011-07-13 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/12057/1/thesis.pdf Abdur, Rakib (2011) Verifying requirements for resource-bounded agents. PhD thesis, University of Nottingham. |
| spellingShingle | Abdur, Rakib Verifying requirements for resource-bounded agents |
| title | Verifying requirements for resource-bounded agents |
| title_full | Verifying requirements for resource-bounded agents |
| title_fullStr | Verifying requirements for resource-bounded agents |
| title_full_unstemmed | Verifying requirements for resource-bounded agents |
| title_short | Verifying requirements for resource-bounded agents |
| title_sort | verifying requirements for resource-bounded agents |
| url | https://eprints.nottingham.ac.uk/12057/ |