If-then-else as a concurrency inhibitor in eager beaver evaluation of recursive programs

Author(s):  
R. L. Page ◽  
M. G. Conant ◽  
D. H. Grit
Keyword(s):  
1991 ◽  
Vol 14 (2) ◽  
pp. 261-281
Author(s):  
Fred Kröger ◽  
Stephan Merz

We propose a temporal logic based on structures divided into several layers of linear “time scales” and give a sound and complete derivation system. The logic is applied to the formulation and verification of assertions about sequential recursive programs.


Author(s):  
Markus Frohme ◽  
Bernhard Steffen

AbstractThis paper presents a compositional approach to active automata learning of Systems of Procedural Automata (SPAs), an extension of Deterministic Finite Automata (DFAs) to systems of DFAs that can mutually call each other. SPAs are of high practical relevance, as they allow one to efficiently learn intuitive recursive models of recursive programs after an easy instrumentation that makes calls and returns observable. Key to our approach is the simultaneous inference of individual DFAs for each of the involved procedures via expansion and projection: membership queries for the individual DFAs are expanded to membership queries of the entire SPA, and global counterexample traces are transformed into counterexamples for the DFAs of concerned procedures. This reduces the inference of SPAs to a simultaneous inference of the DFAs for the involved procedures for which we can utilize various existing regular learning algorithms. The inferred models are easy to understand and allow for an intuitive display of the procedural system under learning that reveals its recursive structure. We implemented the algorithm within the LearnLib framework in order to provide a ready-to-use tool for practical application which is publicly available on GitHub for experimentation.


Sign in / Sign up

Export Citation Format

Share Document