Using language inference to verify omega-regular properties

Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha

Research output: Contribution to journalConference article

Abstract

A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general ω-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of ω-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin's L* algorithm for learning regular languages, we develop an algorithm for verification of ω-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called LEVER and use it to analyze some examples.

Original languageEnglish (US)
Pages (from-to)45-60
Number of pages16
JournalLecture Notes in Computer Science
Volume3440
StatePublished - Sep 19 2005
Event11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: Apr 4 2005Apr 8 2005

Fingerprint

Fixpoint
Verify
Learning systems
Transducers
Transducer
Machine Learning
Formal languages
Model checking
Regular Sets
Liveness
Regular Languages
Model Checking
Strings
Safety
Language
Learning

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Using language inference to verify omega-regular properties. / Vardhan, Abhay; Sen, Koushik; Viswanathan, Mahesh; Agha, Gul.

In: Lecture Notes in Computer Science, Vol. 3440, 19.09.2005, p. 45-60.

Research output: Contribution to journalConference article

@article{5ef6b39866dd46ac8af2f17f10458a68,
title = "Using language inference to verify omega-regular properties",
abstract = "A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general ω-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of ω-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin's L* algorithm for learning regular languages, we develop an algorithm for verification of ω-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called LEVER and use it to analyze some examples.",
author = "Abhay Vardhan and Koushik Sen and Mahesh Viswanathan and Gul Agha",
year = "2005",
month = "9",
day = "19",
language = "English (US)",
volume = "3440",
pages = "45--60",
journal = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Using language inference to verify omega-regular properties

AU - Vardhan, Abhay

AU - Sen, Koushik

AU - Viswanathan, Mahesh

AU - Agha, Gul

PY - 2005/9/19

Y1 - 2005/9/19

N2 - A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general ω-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of ω-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin's L* algorithm for learning regular languages, we develop an algorithm for verification of ω-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called LEVER and use it to analyze some examples.

AB - A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general ω-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of ω-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin's L* algorithm for learning regular languages, we develop an algorithm for verification of ω-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called LEVER and use it to analyze some examples.

UR - http://www.scopus.com/inward/record.url?scp=24644453930&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=24644453930&partnerID=8YFLogxK

M3 - Conference article

AN - SCOPUS:24644453930

VL - 3440

SP - 45

EP - 60

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN - 0302-9743

ER -