Learning Formal Models of Parametrized Systems

Zusammenfassung

Passive learning of formal models from observed system behavior has produced a rich body of results for sequential computational models. Extending this success to concurrent systems poses fundamental new challenges: concurrent models are more succinct, often lack a unique minimal representative, and their semantics depends on the interplay of multiple simultaneous processes. A common restriction in prior work on learning of concurrent models is the assumption of a fixed, known number of processes---an assumption that is fundamentally at odds with parametrized systems, which are designed to operate correctly for any number of processes. We summarize our recent work [1,2] on passive learning of broadcast protocols (BPs), a well-studied model of parametrized concurrent systems. For the class of fine BPs--BPs with no hidden state and a finite cutoff--we establish a comprehensive learnability picture: a constraint-based passive learning algorithm that infers a BP consistent with a given sample, returning a minimal equivalent BP when the sample subsumes a characteristic set (CS); hardness results showing that consistency is NP-complete, that CS may be exponentially large, and that fine BPs are not polynomially predictable; along side LeoParDS, the first tool implementing theses techniques in the parametrized setting.