Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: temporal logics

Sortuj według:

Ogranicz wyniki do:

Unbounded Model Checking for ATL

Kański Michał, Niewiadomski Artur, Kacprzak Magdalena, Penczek Wojciech, Nabiałek Wojciech

Studia Informatica : systems and information technology

2021

Vol. 1-2(25)

5--22

In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.

Proving Theorems by Program Transformation

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

2013

Vol. 127, nr 1-4

115--134

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

Bounded Model Cheking for Interpreted Systems

Penczek W., Lomuscio A.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2002

Nr 946

1-8

We present an extension of a bounded model checking algorithm to deal with temporal epistemic formulas. We use the algorithm to solve a variant of the bit transmission problem

W pracy przedstawiamy rozszerzenie algorytmu ograniczonej weryfikacji modelowej do temporalnych formuł epistemicznych. Algorytm jest zastosowany do weryfikacji pewnego wariantu problemu transmisji bitów.