Article

Minimization, learning, and conformance testing of boolean programs

Authors:

Mahesh ViswanathanAuthors Info & Claims

CONCUR'06: Proceedings of the 17th international conference on Concurrency Theory

Pages 203 - 217

https://doi.org/10.1007/11817949_14

Published: 27 August 2006 Publication History

Abstract

Boolean programs with recursion are convenient abstractions of sequential imperative programs, and can be represented as recursive state machines (RSMs) or pushdown automata. Motivated by the special structure of RSMs, we define a notion of modular visibly pushdown automata (modular VPA) and show that for the class of languages accepted by such automata, unique minimal modular VPA exist. This yields an efficient approximate minimization theorem that minimizes RSMs to within a factor of k of the minimal RSM, where k is the maximum number of parameters in any module. Using the congruence defined for minimization, we show an active learning algorithm (with a minimally adequate teacher) for context free languages in terms of modular VPAs. We also present an algorithm that constructs complete test suites for Boolean program specifications. Finally, we apply our results on learning and test generation to perform model checking of black-box Boolean programs.

References

[1]

R. Alur, M. Benedikt, K. Etessami, P. Godefroid, T. W. Reps, and M. Yannakakis. Analysis of recursive state machines. TOPLAS, 27(4):786-818, 2005.

Digital Library

[2]

R. Alur, P. Cerny, P. Madhusudan, and W. Nam. Synthesis of interface specifications for Java classes. In POPL, pages 98-109. ACM Press, 2005.

Digital Library

[3]

R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In TACAS, LNCS 2988, pages 467-481. Springer, 2004.

[4]

R. Alur, V. Kumar, P. Madhusudan, and M. Viswanathan. Congruences for visibly pushdown languages. In ICALP, LNCS 3580, pages 1102-1114. Springer, 2005.

Digital Library

[5]

R. Alur and P. Madhusudan. Visibly pushdown languages. In STOC, pages 202- 211. ACM Press, 2004.

Digital Library

[6]

R. Alur and P. Madhusudan. Adding nesting structure to words. In DLT, LNCS 4036, pages 1-13, 2006.

Digital Library

[7]

R. Alur, P. Madhusudan, and W. Nam. Symbolic compositional verification by learning assumptions. In CAV, LNCS 3576, pages 548-562. Springer, 2005.

Digital Library

[8]

G. Ammons, R. Bodik, and J. R. Larus. Mining specifications. SIGPLAN Not., 37(1):4-16, 2002.

Digital Library

[9]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75:87-106, 1987.

Digital Library

[10]

T. Ball and S. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, LNCS 1885, pages 113-130. Springer, 2000.

Digital Library

[11]

P. Berman and R. Roos. Learning one-counter languages in polynomial time. In FOCS, pages 61-67. IEEE, 1987.

Digital Library

[12]

J. M. Cobleigh, D. Giannakopoulou, and C. S. Pasareanu. Learning assumptions for compositional verification. In TACAS, LNCS 2619, pages 331-346, 2003.

Digital Library

[13]

A. Friedman and P. Menon. Fault Detection in Digital Circuits. PrenticeHall, Inc., Englewood Cliffs, New Jersey, 1971.

[14]

A. Groce, D. Peled, and M. Yannakakis. Adaptive model checking. In TACAS, LNCS 2280, pages 357-370. Springer-Verlag, 2002.

Digital Library

[15]

M. Kearns and U. Vazirani. An introduction to computational learning theory. MIT Press, 1994.

Digital Library

[16]

Z. Kohavi. Switching and Finite Automata Theory. McGraw-Hill, New York, 1978.

Digital Library

[17]

V. Kumar, P. Madhusudan, and M. Viswanathan. Minimization, learning, and conformance testing of Boolean programs. Technical Report UIUCDCS-R-2006- 2736, University of Illinois at Urbana-Champaign, June 2006.

Digital Library

[18]

D. Lee and M. Yannakakis. Principles and methods of testing finite state machines - A survey. In Proceedings of the IEEE, volume 84, pages 1090-1126, 1996.

[19]

R. Linn and M. Üyar. Conformance testing methodologies and architectures for OSI protocols. IEEE Computer Society Press, 1995.

Digital Library

[20]

E. F. Moore. Gedanken-experiments on sequential machines. In Automata Studies, pages 129-153, Princeton University Press, Princeton, NJ, 1956.

[21]

D. Peled, M. Y. Vardi, and M. Yannakakis. Black box checking. J. Autom. Lang. Comb., 7(2):225-246, 2001.

Digital Library

[22]

Y. Sakakibara. Efficient learning of context-free grammars from positive structural examples. Inf. Comput., 97(1):23-60, 1992.

Digital Library

[23]

J. Tretmans. A formal approach to conformance testing. In Protocol Test Systems, volume C-19 of IFIP Trans., pages 257-276. North-Holland, 1994.

Digital Library

[24]

L. Valiant. A theory of the learnable. Comm. of the ACM, 27(11):1134-1142, 1984.

Digital Library

[25]

A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Actively learning to verify safety for FIFO automata. In FSTTCS, LNCS 3328, pages 494-505, 2004.

Digital Library

Cited By

Sistla MChaudhuri SReps T(2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689760
Jia XTan G(2024)V-Star: Learning Visibly Pushdown Grammars from Program InputsProceedings of the ACM on Programming Languages10.1145/36564588:PLDI(2003-2026)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656458
Fisman DSaadon S(2022)Learning and Characterizing Fully-Ordered Lattice AutomataAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_17(266-282)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_17
Show More Cited By

Index Terms

Minimization, learning, and conformance testing of boolean programs
1. Theory of computation
  1. Formal languages and automata theory

Recommendations

Conformance testing of boolean programs with multiple faults
FMOODS'12/FORTE'12: Proceedings of the 14th joint IFIP WG 6.1 international conference and Proceedings of the 32nd IFIP WG 6.1 international conference on Formal Techniques for Distributed Systems

Conformance testing is the problem of constructing a complete test suite of inputs based on a specification S such that any implementation I (of size less than a given bound) that is not equivalent to S gives a different output on the test suite than S. ...
A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiability

We present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSAT_CNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...
Bisimulation Minimisation of Weighted Automata on Unranked Trees

Several models of automata are available that operate unranked trees. Two well-known examples are the stepwise unranked tree automaton (suta) and the parallel unranked tree automaton (puta). By adding a weight, taken from some semiring, to every ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CONCUR'06: Proceedings of the 17th international conference on Concurrency Theory

August 2006

524 pages

ISBN:3540373764

Editors:
Christel Baier
Institute for Theoretical Computer Science, Technical University Dresden, Germany
,
Holger Hermanns
Institute for Theoretical Computer Science, INRIA, VASY, Grenoble Rhône-Alpes, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sistla MChaudhuri SReps T(2024)Weighted Context-Free-Language Ordered Binary Decision DiagramsProceedings of the ACM on Programming Languages10.1145/36897608:OOPSLA2(1390-1419)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689760
Jia XTan G(2024)V-Star: Learning Visibly Pushdown Grammars from Program InputsProceedings of the ACM on Programming Languages10.1145/36564588:PLDI(2003-2026)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656458
Fisman DSaadon S(2022)Learning and Characterizing Fully-Ordered Lattice AutomataAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_17(266-282)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_17
Frohme MSteffen B(2021)Compositional learning of mutually recursive procedural systemsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-021-00634-y23:4(521-543)Online publication date: 1-Aug-2021
https://dl.acm.org/doi/10.1007/s10009-021-00634-y
Heizmann MSchilling CTischner D(2017)Minimization of Visibly Pushdown Automata Using Partial Max-SATProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_27(461-478)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54577-5_27
Prabhakar PViswanathan M(2012)Conformance testing of boolean programs with multiple faultsProceedings of the 14th joint IFIP WG 6.1 international conference and Proceedings of the 32nd IFIP WG 6.1 international conference on Formal Techniques for Distributed Systems10.1007/978-3-642-30793-5_7(101-117)Online publication date: 13-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-30793-5_7
Salomaa K(2011)Limitations of lower bound methods for deterministic nested word automataInformation and Computation10.1016/j.ic.2010.11.021209:3(580-589)Online publication date: 1-Mar-2011
https://dl.acm.org/doi/10.1016/j.ic.2010.11.021
Han YSalomaa K(2009)Nondeterministic state complexity of nested word automataTheoretical Computer Science10.1016/j.tcs.2009.01.004410:30-32(2961-2971)Online publication date: 1-Aug-2009
https://dl.acm.org/doi/10.1016/j.tcs.2009.01.004
Alur RKolaitis PLibkin L(2007)Marrying words and treesProceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems10.1145/1265530.1265564(233-242)Online publication date: 11-Jun-2007
https://dl.acm.org/doi/10.1145/1265530.1265564
Kumar VMadhusudan PViswanathan MWilliamson CZurko MPatel-Schneider PShenoy P(2007)Visibly pushdown automata for streaming XMLProceedings of the 16th international conference on World Wide Web10.1145/1242572.1242714(1053-1062)Online publication date: 8-May-2007
https://dl.acm.org/doi/10.1145/1242572.1242714

View Options

View options

Media

Figures

Other

Tables

View Table of Contents