Aximo is a tool for verifying knowledge in dynamic multi-agent scenarios. The underlying engine is based on the algebraic axiomatics of dynamic epistemic logic. It is the work of Simon Richards and Mehrnoosh Sadrzadeh.
Our paper on the system, 'Aximo: automated axiomatic reasoning for information update', is set to debut in November 2007 at the
5th Methods for Modalities (M4M) conference at the Ecole Normale Superieure de Cachan in France.
11th Feb 2008: Another update to the
M4M5 conference paper has been uploaded.
30th Nov 2007: The
M4M5 conference paper has been updated, and I've also uploaded the demonstration version of Aximo used at the conference (which has assumptions for the muddy children problem built in).
6th Nov 2007: Uploaded a version of the paper which is to be presented at
M4M5 later this month.
14th Sept 2007: Appearance evaluation has been fixed to prevent duplicate states/actions from appearing, improving overall system performance. The input parser has been updated such that all input is now case insensitive and 'help' can be typed in most places to gain a quick reference of what needs to be inputted (syntax etc.). All builds have been updated with the changes.
13th Sept 2007: Fixed a bug which was preventing multiple nested parenthesis to be parsed properly. Additionally, the input checking has been improved to detect when a starting state/ending fact is not present in all decompositions of the inequality. Error messages for bad user input have been updated to reflect this addition. All builds have been updated with the changes.
7th Sept 2007: Compiles for Linux (x86) and Windows are added.
Aximo has been developed primarily on OSX (on an Intel-based machine), so updates for this platform will usually appear first. Windows and Linux versions should work fine, but the OSX build has been more thoroughly tested.
- Aximo (zipped)
- Documents
- Papers
Aximo is an ongoing development, so although it is in a working state, there are still a number of issues to be aware of:
- Text output is really slow, especially under Windows. As the text output is currently inline with the logic code itself this gives a poor representation of Aximo's speed. In later versions it is hoped to provide a separate output interface, with would not only split out the main processing, but also allow for custom outputs.
- Whilst dynamic modalities can exist in kernels and will be correctly handled by the solving engine, such kernels can lead to an infinite loop. Currently, no checking is done to prevent such looping from occurring. As a result, dynamic modalities are not officially supported until infinite loops are correctly detected and eliminated.
- The system asks for all necessary information 'on the fly', but (in most cases) does not keep a cache of previously entries. Consequently, it's possible for the system to ask for the same information twice. Giving different information in such cases may lead to unexpected results.
- Support for reading axioms/assumptions in from a text file is not currently enabled due to implementation issues.
- Whilst every attempt has been to remove them, there may be a few residing memory leaks. This is one of the reasons for wanting to port the algorithm to D (which has garbage collection at the compiler level).
Downloads