[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/800076.802493acmconferencesArticle/Chapter ViewAbstractPublication PagesstocConference Proceedingsconference-collections
Article
Free access

Equations between regular terms and an application to process logic

Published: 11 May 1981 Publication History

Abstract

Regular terms with the Kleene operations ∪,;, and * can be thought of as operators on languages, generating other languages. An equation r1 = r2 between two such terms is said to be satisfiable just in case languages exist which make this equation true. We show that the satisfiability problem even for *-free regular terms is undecidable. Similar techniques are used to show that a very natural extension of the Process Logic of Harel, Kozen and Parikh is undecidable.

References

[1]
G. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, The Temporal Analysis of Fairness, 7th Annual ACM Symposium on POPL, Jan 1980, 163-173.
[2]
D. Harel, Two Results on Process Logic, Information Processing Letters, 8 (1979) 195-198.
[3]
M. Harrison, Introduction to Formal Language Theory, Addison-Wesley, 1978.
[4]
D. Harel, D. Kozen, and R. Parikh, Process Logic: Expressiveness, Decidability, Completeness. Proceedings of the 21st IEEE Symposium on the Foundations of Computer Science. pp 129-142.
[5]
A. Meyer, WSIS is not Elementary Decidable, Logic Colloquium (Ed. R.Parikh), Lecture Notes in Mathematics 453, Springer 1974.
[6]
H. Nishimura, Descriptively Complete Process Logic, typescript, Kyoto University, Dec. 1979.
[7]
R. Parikh, Second Order Process Logic, 19th IEEE Symposium on Foundations of Computer Science, Oct. 1978, pp. 173-183.
[8]
V.R. Pratt, Process Logic, Proc. 6th Ann. ACM Symp. on Principles of Programming Languages, Jan. 1979.
[9]
M. Rabin, Decidability of Second Order Theories and Automata on Infinite trees, Transactions of the American Math Society, 141 (1969) pp1-35.

Cited By

View all
  • (2014)Normal Form Expressions of Propositional Projection Temporal LogicComputing and Combinatorics10.1007/978-3-319-08783-2_8(84-93)Online publication date: 2014
  • (2011)Synthesising Classic and Interval Temporal LogicProceedings of the 2011 Eighteenth International Symposium on Temporal Representation and Reasoning10.1109/TIME.2011.19(64-71)Online publication date: 12-Sep-2011
  • (2010)A Symbolic Execution Framework for JavaScriptProceedings of the 2010 IEEE Symposium on Security and Privacy10.1109/SP.2010.38(513-528)Online publication date: 16-May-2010
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
STOC '81: Proceedings of the thirteenth annual ACM symposium on Theory of computing
May 1981
390 pages
ISBN:9781450373920
DOI:10.1145/800076
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 May 1981

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Acceptance Rates

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25
57th Annual ACM Symposium on Theory of Computing (STOC 2025)
June 23 - 27, 2025
Prague , Czech Republic

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)35
  • Downloads (Last 6 weeks)2
Reflects downloads up to 26 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2014)Normal Form Expressions of Propositional Projection Temporal LogicComputing and Combinatorics10.1007/978-3-319-08783-2_8(84-93)Online publication date: 2014
  • (2011)Synthesising Classic and Interval Temporal LogicProceedings of the 2011 Eighteenth International Symposium on Temporal Representation and Reasoning10.1109/TIME.2011.19(64-71)Online publication date: 12-Sep-2011
  • (2010)A Symbolic Execution Framework for JavaScriptProceedings of the 2010 IEEE Symposium on Security and Privacy10.1109/SP.2010.38(513-528)Online publication date: 16-May-2010
  • (2008)Forays into Sequential Composition and Concatenation in EagleRuntime Verification10.1007/978-3-540-89247-2_5(69-85)Online publication date: 30-Mar-2008
  • (2005)Propositional calculi of term satisfiability and process logicsComputation Theory10.1007/3-540-16066-3_12(118-126)Online publication date: 28-May-2005
  • (2005)Executing temporal logic programsSeminar on Concurrency10.1007/3-540-15670-4_6(111-130)Online publication date: 29-May-2005
  • (2005)Propositional dynamic logics of programs: A surveyLogic of Programs10.1007/3-540-11160-3_4(102-144)Online publication date: 30-May-2005
  • (2005)Compositionality of fixpoint logic with chopProceedings of the Second international conference on Theoretical Aspects of Computing10.1007/11560647_9(136-150)Online publication date: 17-Oct-2005
  • (2004)Regular Language Matching and Other Decidable Cases of the Satisfiability Problem for Constraints between Regular Open TermsSTACS 200410.1007/978-3-540-24749-4_52(596-607)Online publication date: 2004
  • (2002)On non-local propositional and local one-variable quantified CTL*Proceedings Ninth International Symposium on Temporal Representation and Reasoning10.1109/TIME.2002.1027466(2-9)Online publication date: 2002
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media