Emmanuel Paviot-Adet

In Proceedings of the 41th IFIP international conference on formal techniques for distributed objects, components and systems (FORTE’22)

Abstract Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity.

polyDD: Towards a framework generalizing decision diagrams

By Alban Linard, Emmanuel Paviot-Adet, Fabrice Kordon, Didier Buchs, Samuel Charron

2010-06-01

In Proceedings of the 10th international conference on application of concurrency to system design (ACSD)

Abstract Decision Diagrams are now widely used in model checking as extremely compact representations of state spaces. Many Decision Diagram categories have been developed over the past twenty years based on the same principles. Each one targets a specific domain with its own characteristics. Moreover, each one provides its own definition. It prevents sharing concepts and techniques between these structures. This paper aims to propose a basis for a common Framework for Decision Diagrams.

LTL under reductions with weaker conditions than stutter invariance

polyDD: Towards a framework generalizing decision diagrams

Search

Tags