Workshop on Formal Methods and Artificial Intelligence for Logistics (FMAIL)

Bergen, Norway

December 2

Colocated with iFM 2019

Context and Goals

Logistics is the process of planning, implementing and controlling procedures for the efficient and effective transportation and storage of goods including services and related information from the point of origin to the point of consumption for the purpose of conforming to customer requirements. Planning is the process of identifying, scheduling and tracking activities needed to achieve a specific goal, be it in the area of maintenance, production or development. The resulting work plans serve as input and trigger for logistics, and are in turn influenced by it. Logistics 4.0 advocates the universal digitalisation of the whole supply chain to help to automate, verify and coordinate the execution of the procedures among the different stakeholders involved, in nearly real-time, enabling a faster reactivity and resources savings. It includes especially also methods for accounting and contract negotiations between the stakeholders, a field addressed in AI. The workshop is dedicated to the advancement of the theory and practice for software systems and processes dedicated to logistics and planning. The goal is to provide a symposium for engineers, researchers and business specialists to exchange experiences and problematics in the area. Original research and experience contributions on the principles, design, implementation, modelling, analysis, verification, and application of Software or Decision Procedures for logistics systems are solicited.

Topics of Interest

Here are some suggested topics that are of interest to this workshop:


Dates and Venue

The workshop will take place in Bergen, Norway from December 2, 2019. The workshop will take place in the Kronstad Campus of Western Norway University of Applied Sciences . For more details, see iFM.


Participants to the workshop must register using the procedure for iFM.

List of Confirmed Speakers

Tentative Program

Monday 2 December 19
09:00-10:00 Francesco Leofante AI Planning meets Production Logistics
10:00-10:30 Coffee break
10:30-11:30 Thomas Troels Hildebrandt Distributed Declarative Contracts with Dynamic Condition Response Graphs
11:30-12:00 Ralf Möller Reputation Models for Tipping the Scales in Automatic Negotiation and Decision Making
12:30-14:00 Lunch
14:00-15:00 Fritz Henglein Smart digital contracts for next-generation distributed ledger technology
15:00-15:30 Industrial panel discussion
15:30-16:00 Coffee break
16:00-17:00 Gerardo Schneider Formalisation and Analysis of Normative Documents
17:00-17:30 Closing session


Planning for logistics requires algorithms and tools that can handle the challenges such scenarios pose. On the one hand, expressive languages are needed to build faithful models; on the other hand, efficient solving techniques that can support these languages need to be devised.
The existence of this trade-off, however, does not mean progress is not possible!
Using the RoboCup Logistics League as a testbed, I will focus on production logistics and show how recent advances in satisfiability checking can be used to solve some interesting problems in the field.

In the talk we present the formal background, tools and applications of the Dynamic Condition Response (DCR) Graph modelling notation and technology stack developed during the last 10 years, leading to the establishment of the company in 2018 as part of the research project.
DCR Graphs is an event-based declarative process notation generalizing event structures to allow finite models of infinitary, timed processes with data. The notation can capture both prohibitions and obligations, capturing distributed contracts with both safety and liveness properties. The DCR notation is supported by a full technology stack (available at and consisting of a web-based design and simulation tool , a process engine, declarative process mining, and an open source case management tool. There is also a natural language process mapping tool allowing NLP supported mapping from natural language contract specifications to DCR process models.
Finally, there is a prototype block-chain execution engine. The technology is available for academic use by joining the DCR academic community and can be licensed for commercial use. Today the DCR process engine is build into workflow and case management systems widely used in the Danish governmental sector. Documentation and access to tools can be found at

In this talk I will give an overview of the work I have been involved in since 2006 concerning the formalisation and analysis of normative documents. I will briefly present the formal language CL and C-O Diagrams, which allow for the representation of norms containing obligations, permissions and prohibitions, as well as their associated penalties. I will also talk about a framework (and a prototype tool) that takes natural language normative documents and gives a CNL (controlled natural language) as well as a formal model amenable to syntactic and semantic queries. I will then discuss the connection between smart contracts and the legal world and will give a proposal to bridge the existing gap between them.

Blockchain and distributed ledger (BC/DL) technology provides a conceptual, economic and technical platform for decentralized management of information and economic resources ("tokenized" money, goods, assets, rights, etc). It guarantees that stored information cannot subsequently be modified or deleted and that resources can only be transferred, not copied (forged or duplicated). Modern BC/DL systems support installing and executing user-defined programs, called smart contracts.
We present a deconstruction of BC/DL systems and smart contracts that reflects a contract-centric view of business interaction: formally specified contracts specify permissions and obligations; contract managers are robotic agents (programs) that monitor and manage contracts; and resource managers are systems that maintain authoritative information on resource ownership. Resource and contract managers may be decentralized or centralized. This facilitates an open ecosystem of BC/DL systems and conventional cloud/server-based systems.
Based on joint work with the Deon Digital Denmark research and development team.

In the presentation we consider how models of reputation can be incorporated into models for negotiation and decision making based on optimizing expected utility used in agent systems. In order to evaluate basic modeling options, we consider a stylized application of STaRAI (STochAstic Relational AI) in a logistics domain.


Sirius logo

Photo by Tyler Casey.