|
Overview
In recent years data-aware systems have been proposed as a comprehensive framework to model complex business workflows by considering data and processes as equally relevant tenets of the system
description.
The SVeDaS project is designed to advance the state-of-the-art in the modelling, analysis and deployment of data-aware systems by
using a novel, compositional, agent-based approach to their specification and verification, and to apply these results to the verification of auctions against strategic behaviours of agents,
such as collusion and manipulation.
The main objectives of the SVeDaS project can be summarized as follows:
- to introduce agent-based, computationally-grounded models for data-aware systems, that are capable of expressing rich business
workflows, including auction-based mechanisms in e-markets;
- to explore logic-based formal languages for the specification of strategic behaviours of autonomous agents (including robustness
against malicious behaviours in auctions) pertaining to business processes and agents operating on them;
- to analyse the formal properties of these data-aware models, particularly the issues concerning formal verification by model
checking in contexts of imperfect information;
- to find classes of data-aware systems and expressive language fragments relevant for auction-driven applications, which have a
decidable model checking problem and possibly are also amenable to practical verification;
- to develop the model checker SVeDaS for the verification and validation of data-aware systems in multi-agent scenarios;
- to evaluate the performance of the SVeDaS tool in popular auctioning mechanisms, including real-time bidding, and to release
SVeDaS as open-source software.
We anticipate that the results of the SVeDaS project will contribute significantly to our understanding of data-aware systems, thus
improving the design and management of business processes by formal verification through model checking, including through the model
checker SVeDaS. In turn, these contributions will help building more secure and reliable auction-based mechanisms for e-commerce and e-
business.
List of publications
2019
2018
2017
- F. Belardinelli, U. Grandi, A. Herzig, D. Longin, E. Lorini, A. Novaro, L. Perrussel; Relaxing Exclusive Control in Boolean Games. TARK17.
- F. Belardinelli, A. Herzig; Dynamic Logic for the Verification of
Data-aware Systems: Decidability Results. IJCAI17.
- F. Belardinelli, P. Kouvaros,
A. Lomuscio; Parameterised
Verification of Data-aware Multi-agent Systems. IJCAI17.
- F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin; Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic. IJCAI17.
- F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, A. V. Jones; Bisimulations for Verifying
Strategic Abilities with an Application to ThreeBallot. AAMAS17.
- F. Belardinelli, A. Lomuscio, A. Murano, S. Rubin; Verification of Multi-agent Systems with Imper-
fect Information and Public Actions. AAMAS17.
- F. Belardinelli, A. Lomuscio; Agent-based Abstractionsv for Verifying Alternating-time Temporal
Logic with Imperfect Information. AAMAS17.
|