figure b

1 Introduction

In this paper, we present a new model checker called EPMC, an acronym for Extendible Probabilistic Model Checker. Two main characteristics of EPMC are its high modularity and its full extendibility. It achieves its flexibility by an infrastructure that consists of a minimal core part and multiple plugins that provide model checking functionalities. We believe that it is very convenient to develop a new model checker based on the core parts of EPMC. While the model checker historically starts from probabilistic models, it will be easy to extend it to incorporate other model types.

The baseline includes model checking functionality for probabilistic systems. Probabilistic systems play an important role in reasoning about randomised network protocols, and biological and concurrent systems. They also find applications in analysing security protocols. Markov decision processes are among the most important semantic models. As a result, several model checkers that support MDP analysis have been developed, including the state-of-the-art probabilistic model checker PRISM  [35], Storm  [15], MRMC  [30], LiQuor  [12], MoChiBa  [50], and IscasMc  [22]. These model checkers differ in the model and property types they support. For instance, MRMC and Storm handle branching time properties specified in PCTL [25], whereas LiQuor, IscasMc and MoChiBa are specialised in analysing linear time properties (PLTL) [5]. PRISM can handle both.

The first baseline of EPMC includes support for PCTL, PLTL, and their extension to PCTL*. In addition, it can also be used to analyse Markov games. To demonstrate the main features of EPMC, we extend it to the model checker EPMC-petl. EPMC-petl is designed for the verification of probabilistic multi-agent systems against PETL (probabilistic epistemic temporal logic) properties under uniform schedulers. Multi-agent systems have found many applications and verification techniques have also been proposed over the past decades. Although there are model checkers for multi-agent systems, as we will see in related works (Sect. 4), they can only handle restricted classes of the model we are interested in, such as a non-probabilistic setting or, where they can handle probability, they do not support epistemic accessibility relations. The algorithmic design, implementation, and validation based on an existing model checker for probabilistic multi-agent systems against properties specified in PETL under uniform schedulers is not available.

Exploiting the minimal kernel and multiple plugins of EPMC, we can conveniently implement the algorithms specific for the epistemic fragment of PETL while reusing the core parts of EPMC for the management of the remaining fragment, part of PCTL. In particular, the modularity of EPMC makes the development of new functionalities rather independent from the existing ones, without having to change existing code. This speeds up the implementation and simplifies the debugging of the code, by isolating the different components responsible for the different verification steps.

Summarising, the main features of EPMC include extendibility, modularity, and the support of games and strategy synthesis. Beyond introducing EPMC, we also present, with its extension to EPMC-petl, the first tool that supports PETL model checking for probabilistic nondeterministic multi-agent systems.

Organisation of the Paper. Section 2 introduces the architecture of our tool. In particular, we demonstrate how to develop the PETL model checker EPMC-petl. Experimental results are presented in Sect. 3. Sect. 4 discusses related works, and Sect. 5 concludes the paper.

2 Architecture

We show the architecture of EPMC and how to build EPMC-petl on top of it. EPMC contains two main components: a) EPMC core; b) various plugins. Details of these components and the interface are provided below.

The larger part of EPMC is developed in Java. It uses JNA [3] to access libraries written in C/C++ to improve the performance of some computation or to provide access to legacy code. Instances of such libraries are the BDD libraries (like CUDD [51]) used to store symbolically the models or the C implementation of different versions of value iteration algorithms. The compilation of EPMC is managed by the software project management and comprehension tool Maven [2]. Maven takes care of caching and retrieving all building dependencies such as Ant [1] and JavaCC [4], used for the parsers. This allows for porting EPMC to multiple platforms and architectures.

2.1 EPMC Core

EPMC consists of a minimal kernel and multiple plugins that provide the functionalities needed for model checking. This kernel is rather small. It is only responsible for the bootstrap phase, where the plugins are loaded, and for starting the model checking procedure. It first initialises the data structures needed to load the plugins and then loads and initialises each plugin according to the order, in which they are specified. Finally, it starts the model checking procedure by parsing the given models and properties and calling the appropriate solvers.

In order to maximise modularity, the kernel has no information about the existing plugins until they are loaded and initialised; it is the duty of each plugin to register itself in EPMC. In order to be recognised as a valid EPMC plugin, it has to

  • declare its name and that it is an EPMC plugin in its MANIFEST.MF file;

  • list the plugins it depends on; and

  • implement all interfaces defined by the plugin manager from the kernel part.

Once the plugin meets these requirements, it can be used in EPMC to provide the expected functionalities. The plugin can be inserted into EPMC in two ways: either its jar file is placed in the embeddedplugins directory contained in the EPMC jar file and its name is listed in the embeddedplugins.txt file; or it is specified at command line by means of the option plugin as a jar file or as a directory containing the class files. During the kernel’s bootstrap phase, the plugins listed in embeddedplugins.txt are loaded first, following the order in which they appear in the file. Then the plugins specified by the option plugin are loaded according to their order.

When loading a plugin, a set of specific methods defined by the plugin interface are called. In these methods, the plugin can register itself with respect to its functionalities. A plugin can, for example, add new command line options, new commands, or new data types; or it can declare to support specific operations, such as model checking a specific logic operator. The registration performed by a plugin can be altered by the plugins loaded later. A plugin loaded later has therefore a higher priority than a plugin loaded earlier. In particular, one can last load a simple plugin that removes or modifies some of the options provided earlier in order to create a version of EPMC specialised for specific tasks within a specific setting.

2.2 Plugins Available in EPMC

We will now introduce some of the plugins natively supported by EPMC; the different flavours of EPMC can be obtained by choosing and combining multiple plugins together: for instance, by selecting the appropriate set of plugins EPMC becomes a tool for performing PCTL model checking on Markov chains or MDPs, and with a different set of plugins we can obtain a tool for model checking Markov decision processes against PLTL formulas. By combining the two sets of plugins, the resulting EPMC is able to check these models against the whole of PCTL*. Below we give an overview of the plugins of EPMC.

Algorithm Group: This group contains all plugins that provide the classical algorithms that are used for probabilistic model checking, such as graph decomposition into strongly connected components and maximal end components for both symbolic and explicit representations. It currently only includes the plugin algorithm, which provides standard algorithms, such as the following ones: FoxGlynn, which follows the algorithm proposed in [28] for computing Poisson probabilities for CTMCs; Tarjan, which implements the well-known strongly connected component decomposition algorithm by Robert Tarjan [53] for explicit data structures; and Bloem and Chatterjee, which compute strongly connected components using BDDs and are based on the work of Roderick Bloem et al. [6] and Krishnendu Chatterjee et al. [10], respectively.

Automata Group: The purpose of this group is to enclose the plugins that encode \(\omega \)-regular automata. It currently includes two plugins, namely the automata and the automaton-determinisation plugins. automata provides a uniform interface for automata such as Büchi and Rabin automata, while automaton-determinisation provides the algorithms proposed by Sven Schewe, Thomas Varghese, and Nir Piterman [46, 48, 49] to determinise nondeterministic Büchi automata to deterministic Rabin and parity automata.

Command Group: This group provides three plugins that set the main functionality of EPMC: command-check calls the model checker to actually perform the model checking operation; command-help prints out the usage messages; and command-lump requires as input a probabilistic model and generates as output a new model, which is bisimilar to the original model.

BDD Group: The BDD group is dedicated to the symbolic representation of models and properties by means of the Binary Decision Diagrams data structures. The dd plugin provides a uniform interface to use a BDD library and therefore does not provide any actual implementation of BDD data structures. Such an implementation is provided by one of the following plugins; each of them implements the dd interface and at least one of them has to be included whenever EPMC is expected to support the symbolic representation of models.

The dd-buddy plugin wraps the C library BuDDy [14], which is a small and efficient BDD library. The dd-cacbdd plugin gives access to the C++ library CacBDD [44], which implements a dynamic cache management algorithm. The dd-cudd plugin provides the C library CUDD [51], which is the most well-known BDD library used in several tools; it is the default BDD library of the PRISM model checker [35, 47]. The dd-cudd-mtbdd plugin is the companion of dd-cudd for the multi-terminal binary decision diagrams (MTBDDs) offered by CUDD. The dd-jdd plugin includes the library JDD [54], which is a Java implementation of binary decision diagrams inspired by BuDDy. The dd-sylvan and dd-sylvan-mtbdd plugins make the library Sylvan [17] available in EPMC; Sylvan is a parallel (multi-core) BDD library written in C.

Bisimulation Algorithm Group: This group collects the plugins that compute bisimulation relations on the models: the lumper-explicit-signature plugin implements a signature based lumping algorithm for probabilistic systems; and the lumper-dd plugin implements a lumping algorithm for probabilistic systems by using MTBDDs.

Expression Group: This group hosts the expression-basic plugin, which is designed to provide a uniform interface as well as the corresponding data structures to handle formulas from temperoal logics like PCTL and PLTL.

Graph Group: The single graph plugin available in this group provides a uniform interface as well as the data structures to store various models as a graph. The model can be a Markov chain, a Markov decision process, an automaton, or any model that can be interpreted as a labelled graph. It also provides the interfaces to access the properties in the nodes or the properties on the edges. For instance, it permits to collect all atomic propositions that hold in a state via evaluating the properties of this state node.

Graph Solver Group: Similar to the BDD group, we have the graphsolver plugin, which defines a uniform interface for solving the linear programming problems used to compute the reachability probabilities the model checking problems are reduced to. The actual implementation is provided by the graphsolver-iterative plugin, which solves the given linear programming problem by value iteration. It supports both Jacobi and Gauss-Seidel iteration methods.

JANI Format Group: This group contains all plugins related to the recently proposed JANI model and interaction format [7]. There are currently three plugins: the jani-model plugin provides a parser to transform an input JANI model to a graph or an MTBDD. It is also able to parse the input JANI formula; the jani-exporter takes care of exporting models and properties in JANI format.

PRISM Format Group: The single prism-format plugin available in this group provides a parser to transform a given PRISM model description to an explicit graph or an MTBDD. It also provides a parser for the input formula.

Property Solver Group: The plugins contained in this group are responsible for solving the properties analysed during the model checking phase. Similarly to the BDD group, the specific property solvers are all implementations of the common interface provided by the propertysolver plugin. There are currently eight implementation plugins representing eight different classes of properties: propertysolver-coalition provides a solution to solve a probabilistic parity game against linear temporal properties; propertysolver-filter handles the filter operation in the given PRISM formula; propertysolver-ltl-lazy implements an efficient method to model check the PCTL* logic over the probabilistic systems by means of advanced LTL verification techniques; propertysolver-operator works with the operators that occur in the given formula; propertysolver-pctl implements the PCTL model checking algorithm over probabilistic systems; propertysolver-propositional provides a way to identify all states that satisfy the given propositional formula; propertysolver-reachability exemplifies how to write a plugin that handles the reachability formula \(\mathbb {P}_{\mathord {\mathbf {F}}a}\) over Markov chains; and propertysolver-reward implements a model checking algorithm to handle probabilistic systems with rewards.

Util Group: The single plugin util available in this group provides basic utilities useful for working with bits, JSON documents, and other native data types in a JAVA-style approach.

Value Group: Similar to the expression group, this group hosts the value-basic plugin, which is designed to provide a uniform interface to represent all kinds of values and types that may be used in EPMC, as well as the implementation of the standard values and type such as Booleans, integers, and reals.

Dependencies Between Plugins. Each plugin may have build-time and run-time dependencies on other plugins. Build-time dependencies can be considered as hard dependencies: they must be satisfied at compilation time as well as during the bootstrap phase; these build-time dependencies are made explicit in the MANIFEST.MF file, and the order the plugins are loaded in the bootstrap phase has to respect such build-time dependencies. For instance, the property-solver-pctl plugin has a build-time dependency on property-solver, since property-solver-pctl implements the interfaces defined by property-solver.

The graph of build-time dependencies between the groups of plugins is shown in Fig. 1, where an arrow from one group to another means that the former requires the latter. To simplify the graph, we omitted all arrows that can be inferred by transitivity, such as the one between any group and util.

Fig. 1.
figure 1

Build-time dependencies between groups of plugins in EPMC

Full size image

Run-time dependencies can be seen as soft dependencies: their satisfaction depends on the actual steps performed during the model checking phase. For instance, the property-solver-pctl plugin has only a run-time dependency on graphsolver-iterative, since graphsolver-iterative is required during the model checking phase only in cases the property cannot be decided via a simple graph exploration. (This happens for quantitative properties.) This means that graphsolver-iterative has to be available at run-time for some properties, while for other properties it may be missing. If EPMC is intended to be used to check only qualitative properties, then graphsolver-iterative can safely be omitted, while EPMC needs the graphsolver-iterative plugin (or any other plugin implementing graphsolver) to analyse quantitative properties.

Fig. 2.
figure 2

Architecture of EPMC-petl

Full size image

2.3 PETL Model Checker as a Plugin

The structure of EPMC-petl, largely shared with EPMC given its modular architecture, is illustrated in Fig. 2.

To provide the PETL model checking algorithms for multi-agent systems offered by EPMC-petl, we have developed the PETL plugins that add the corresponding functionalities, namely: the parser for the multi-agent system model specification and the PETL properties; the data structures to store them; and the algorithms for evaluating the properties against the given model.

In multi-agent systems, the agents have the capacity to perform certain actions, which they choose according to their individual protocols. Given the distributed nature of multi-agent systems, it is typical that the agents have incomplete information about the state of the global system due to the fact that they are only able to observe a limited part of the global state when they have to choose their actions. The incompleteness of information is normally modelled by defining, for each agent i, an equivalence relation \(\mathord {\sim }_{i}\) over all global states of the systems, then two global states are considered indistinguishable for a given agent i if they are related by \(\mathord {\sim }_{i}\). Note that two states that are indistinguishable for an agent may be distinguishable for another agent, so there is no constraint on how two states are related by the different relations. Every agent makes its own decisions based only on the limited information it has, namely, the information restricted by its own indistinguishability relation. Decisions of agents are usually formalised by schedulers, which are functions that take the history executions as input and decide (output) the next move for each agent. Schedulers that only make use of the limited information each agent is aware of are called uniform. Intuitively, a uniform scheduler for the agent i is expected to make the same choice when given two executions that are equivalent under \(\mathord {\sim }_{i}\).

To build the model checker EPMC-petl, we have to first implement three things in this plugin: the model, the property, and the equivalence relations.

Model. We use the PRISM language as input format and the model type should be “mdp”, to represent the fact that the model has both probabilistic and nondeterministic behaviour. Each module in the MDP defines one agent’s behaviour, with the name of the module being the agent’s name. The state space of the overall multi-agent system is constructed following the PRISM approach, i.e., by considering all state variables, whether local to a module or global, and with the usual PRISM restrictions on how transitions can update these variables.

Differently from the standard PRISM language semantics, at each step every agent chooses one action among the enabled transitions, independent of whether other agents have a transition with the same action that is enabled. The actions labelling the transitions are therefore not used for the synchronisation of the modules: they are instead the names of local actions, and each command must be labelled by one action.

The overall result is that the agents do not interact with each other by synchronising on common actions, but by the effects of the individual transitions chosen by the individual agents.

Property. To specify the properties of probabilistic multi-agent systems, in particular the temporal dynamics of agents’ knowledge, we adopt the probabilistic epistemic temporal logic (PETL) (cf. [16]), which can be viewed as a combination of epistemic logic [18] and probabilistic computation tree logic (PCTL) [25]. To specify PETL formulas, we extend the PRISM language by adding the epistemic operators \(\mathbf {K}_{i}\) and \(\mathbf {E}_{G}\), \(\mathbf {C}_{G}\), and \(\mathbf {D}_{G}\) to the set of operators that can occur in a property formula, where i is (the name of) an agent and G is a set of agents. Intuitively, the property \(\mathbf {K}_{i}\varphi \) means that agent i knows that property \(\varphi \) holds in state s if \(\varphi \) holds in all states equivalent to s with respect to \(\mathord {\sim }_{i}\); properties \(\mathbf {E}_{G}\varphi \), \(\mathbf {C}_{G}\varphi \), and \(\mathbf {D}_{G}\varphi \) are similar, but refer to the common/distributed knowledge of the group of agents. These epistemic operators are thus added to the PRISM properties as K {agent} and E/C/D {agent\(_1\), ..., agent\(_n\)}, respectively.

Equivalence Relations. Equivalence relations are encoded as sets of formulas shown in Fig. 3. Each agent in the model has its own equiv agent_name ...equiv end block and each block contains a set of formulas. The formulas are defined on all state variables that occur in the model definition and are not restricted to those of the corresponding single agent.

Fig. 3.
figure 3

The format of equivalence relations

Full size image

Each formula induces one equivalence class, i.e., two states that satisfy the same formula of agent j are considered to be related by \(\mathord {\sim }_{j}\). This means that formulas are required to be pairwise disjoint; if a state does not satisfy any formula, it is not equivalent to any other state, so it belongs to its singleton equivalence class.

PETL Solvers. In general, the model checking problem for probabilistic multi-agent systems against PETL properties is undecidable [20], but is decidable when restricted to the class of uniform memoryless schedulers. The decision algorithm for the latter follows the PCTL approach: the PETL property is checked bottom-up, with each operator managed by its corresponding solver. Epistemic operators are part of the state formulas while the temporal operators are managed as in PCTL, except for the class of schedulers considered for computing the Until operator.

The key parts of the PETL plugins are three solvers needed to verify PETL properties: the first one focuses on the knowledge operators, while the other two take care of the PCTL until operator (wrapped inside a probabilistic operator \(\mathbb {P}_{}\), as in PCTL), which needs to be computed on the class of uniform memoryless schedulers instead of the general class of memoryless schedulers as done in PCTL; these two solvers implement two different algorithms, an exact one based on mixed integer non-linear programming and an approximation based on upper confidence bounds applied to trees (UCT) [31]. The remaining fragments of PETL, like propositional formulas and the next operator, can be computed as for PCTL. They can therefore be inherited from the existing plugins of EPMC.

MINLP Solver. This solver implements the PETL model checking algorithm developed in [20]: it reduces the problem of checking the satisfaction of an until formula to a mixed integer non-linear programming (MINLP) problem, which can then be solved by, e.g., an SMT solver. Here we make use of the SMT solver Z3 [45], which can be replaced by any other SMT solver that supports SMT-lib version 2.5 as input format. The reduction ensures that the resulting scheduler is uniform and memoryless, with a different encoding for \(\mathbb {P}_{\!\mathrm {max}=?}\) and \(\mathbb {P}_{\!\mathrm {min}=?}\).

UCT Solver. This solver implements an approximated algorithm relative to the until operator, based on the upper confidence bounds applied to trees (UCT) algorithm [19]. This UCT based solver performs a Monte Carlo sampling of the model, with heuristics guiding the choice between the exploration of new parts of the state space, the analysis of already explored state space, and the action to choose. This solver offers several parameters to the user to tune the heuristics: time limit – how much time the solver should use when exploring the model; depth limit – how many steps the solver should perform in the state space exploration; B value – the bias parameter in the UCT formula between old and new state exploration; and random seed – the random seed used to select unvisited successors (so to be able to reproduce the solver’s execution).

The implementation of this solver makes use of specialised data structures to store the information collected during the UCT sampling; in particular, the data structure organises the information so to ensure that the underlying scheduler is uniform, as required by the PETL decision algorithm. The basic idea is to store the selected actions of each agent, and then exclude the actions making the scheduler non-uniform when executing the next step in the exploration.

Knowledge Solver. This solver deals with the knowledge operators, namely \(\mathbf {K}_{i}\), \(\mathbf {E}_{G}\), \(\mathbf {D}_{G}\), and \(\mathbf {C}_{G}\). Depending on the actual knowledge property \(\mathbf {Z}(\varphi )\), the solver takes the satisfaction information about the state formula \(\varphi \) already computed (recall that PETL model checking is based on a bottom-up approach similar to PCTL) and returns the set of states that satisfy \(\mathbf {Z}(\varphi )\), by implementing the semantics of \(\mathbf {Z}(\varphi )\).

Online Availability. EPMC, including its extension EPMC-petl, is an open source tool. EPMC is freely available at https://github.com/ISCAS-PMC/ePMC as a git repository to be forked and modified.

Table 1. Different variations of EPMC. The runtime is given in seconds, and ‘ns’ and ‘to’ abbreviate ‘not supported’ and ‘time-out’ (set to 100 s, as performance was not our concern). The properties used were (PCTL); \(\varphi _{2} = \mathbb {P}_{\!\mathrm {min}=?}[(\mathord {\mathbf {GF}}\text {p1}!=10 \vee \mathord {\mathbf {GF}}\text {p1}=0 \vee \mathord {\mathbf {FG}}\text {p1}=1) \wedge \mathord {\mathbf {GF}}\text {p1}!=0 \wedge \mathord {\mathbf {GF}}\text {p1}=1 ]\) (PLTL); (PCTL); (PLTL); (Coalition); (Coalition); (Coalition); (Coalition); \(\varphi _{9} = \mathbb {P}_{\!\mathrm {max}=?}[\mathbf {G}{ ( rw\_x \ne rc\_x \vee rw\_y \ne rc\_y )}]\) (PETL); and \(\varphi _{10} = \mathbb {P}_{\!\mathrm {max}=?}[\mathbf {G}{\mathbf {E}_{ rw , rc }( rw\_x \ne rc\_x \vee rw\_y \ne rc\_y )}]\) (PETL).
Full size table

3 Empirical Evaluation

We have generated five different flavours of EPMC by loading different modules. One version that supports only PCTL; one that supports PCTL*; one for solving probabilistic parity games; one that supports PETL; and a version that supports all of these. As comparison, we considered the following tools PRISM [35], PRISM-games [11], and Rabinizer4 [34].

We have run these tools on a few MDP benchmarks taken from the PRISM website [47], SMG games from [23, 24] and multi-agent systems from [20]; we considered some simple properties for these models. The goal of the comparison, reported in Table 1, is to show the adaptability of EPMC in supporting different logics and to use different modules, not the actual performance.

4 Related Work

We have already discussed related probabilistic model checkers in the introduction, all of which do not support PETL model checking. Here we list related tools for analysing multi-agent systems or epistemic logics.

MCMAS [41,42,43] is an open-source, OBDD-based symbolic model checker for verifying multi-agent systems. MCMAS is restricted to non-probabilistic models. There are some model checkers for multi-agent systems built on top of MCMAS: MCMAS-SDD [36] introduces an SDD-based technique for the formal verification of multi-agent systems; MCMAS-SLK [8] supports the verification of systems against specifications expressed in strategy logic (SL) with knowledge; MCMAS-SL[1G] [9] puts forward an automata-based methodology for verifying and synthesising multi-agent systems against specifications given in SL[1G], which is the one-goal fragment of strategy logic; MCMAS\(_{LDLK}\) [32] can verify properties given in LDLK (Linear Dynamic Logic with Knowledge) for multi-agent systems; MCMAS\(_{LDL_fK}\) [33] implements the algorithm for the verification of multi-agent systems against \(LDL_fK\) specifications, which is LDLK interpreted on finite traces. As for MCMAS, all these model checkers do not consider probabilistic components in their systems and logics.

Probabilistic swarm systems support systems with an unbounded and time-changing number of agents. Based on PRISM  [35], Lomuscio and Pirovano have introduced the software package PSV (probabilistic swarm verifier), with several sub-components that support bounded time PSV-BD [38], counter abstraction PSV-CA [39], strategic properties PSV-S [40], and faulty systems. The logics these tools consider are either without epistemic operators, or they allow only a single epistemic operator to occur as the top operator of the formula. While the EPMC extension EPMC-petl we have discussed only analyses systems with a fixed number of agents, it supports the nesting of epistemic operators as well as their boolean combination.

MCK [21] is an OBDD-based model checker for multi-agent systems that supports temporal-epistemic specifications. It has been extended in [26] to support probabilistic reasoning, but nondeterministic choices are not considered; the work in [27] implements a symbolic BDD-based model checking algorithm for an epistemic strategy logic with observational semantics also based on MCK. Epistemic accessibility relations are studied in this work, but only for a non-probabilistic setting. EPMC-petl supports the analysis of systems that combine nondeterminism and probabilistic choices, which is missing in these tools.

MCTK [52] is a symbolic model checker for a temporal logic of knowledge. It is developed from NuSMV [13]. Similarly, the authors of [37] propose a methodology for model checking a temporal-epistemic logic by building upon an extension of NuSMV. Verics [29] is a model checker for real-time and multi-agent systems. It implements bounded model checking algorithms for CTL, real-time CTL, and variants of CTL that include epistemic operators. Again, these tools can only work with non-probabilistic multi-agent systems.

5 Conclusion

In this paper we have presented EPMC, an extendible probabilistic model checker, and EPMC-petl, a tool for model checking epistemic properties on multi-agent systems that exhibit both probabilistic and nondeterministic behaviours. Key advantages of EPMC are its high degree of modularity and full extendibility. We have exemplified by the particular extension of EPMC-petl how this extensibility can be used to easily cover attractive new properties that no other solver has covered before. Of course, besides demonstrating this advantage of EPMC, EPMC-petl also provides this additional functionality, which is novel and a contribution in itself.