DocumentCode :
626316
Title :
Regular Real Analysis
Author :
Chaudhuri, Swarat ; Sankaranarayanan, Sriram ; Vardi, Moshe Y.
Author_Institution :
Rice Univ., Houston, USA
fYear :
2013
fDate :
25-28 June 2013
Firstpage :
509
Lastpage :
518
Abstract :
We initiate the study of regular real analysis, or the analysis of real functions that can be encoded by automata on infinite words. It is known that ω-automata can be used to represent relations between real vectors, reals being represented in exact precision as infinite streams. The regular functions studied here constitute the functional subset of such relations. We show that some classic questions in function analysis can become elegantly computable in the context of regular real analysis. Specifically, we present an automatatheoretic technique for reasoning about limit behaviors of regular functions, and obtain, using this method, a decision procedure to verify the continuity of a regular function. Several other decision procedures for regular functions-for finding roots, fixpoints, minima, etc.-are also presented. At the same time, we show that the class of regular functions is quite rich, and includes functions that are highly challenging to encode using traditional symbolic notation.
Keywords :
automata theory; computability; formal languages; ω-automata; automata theoretic technique; computability; decision procedure; fixpoint finding; infinite streams; infinite words; limit behavior; minima finding; real function analysis; real vectors; reasoning; regular function continuity; regular real analysis; relation representation; root finding; symbolic notation; Automata; Calculus; Cognition; Educational institutions; Encoding; Fractals; Vectors; Automata; Decision procedures; Real analysis;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2013 28th Annual IEEE/ACM Symposium on
Conference_Location :
New Orleans, LA
ISSN :
1043-6871
Print_ISBN :
978-1-4799-0413-6
Type :
conf
DOI :
10.1109/LICS.2013.57
Filename :
6571583
Link To Document :
بازگشت