PV1 ⊧ KMCchecks compatibility of communicating automata

Tool for checking k-multiparty compatibility in communicating session automata

Application domain/field

• Communicating automata
• Session types

Type of tool

Property checker

Expected input

• System of communicating automata
• bound MAX

Format:

• System of communicating automata: text file, with either syntactical session types or CFSMs (same input language as GMC)
• Bound: passed as an argument when calling KMC

Expected output

? (seems to be yes or no to indicate whether the system of automata is k-multiparty compatible)

Internals

k-multiparty compatibility is decomposed into two bounded properties:

1. k-safety: within the bound, all sent messages can be received and each automaton can make a move
2. k-exhaustivity: all k-reachable send actions can be fired within the bound