Article

Free access

Reasoning about fair concurrent programs

Authors:

C Courcoubetis,

M Y Vardi,

P WolperAuthors Info & Claims

STOC '86: Proceedings of the eighteenth annual ACM symposium on Theory of computing

Pages 283 - 294

https://doi.org/10.1145/12130.12159

Published: 01 November 1986 Publication History

PDF eReader

References

[1]

K. Abrahamson, "Decidability and Expressiveness of Logics of Programs", Ph.D. Thesis, University of Washington at Seattle, 1980.

Digital Library

Google Scholar

[2]

M. Ben-Ari, Z. Manna, A. Pnueli, "The Temporal Logic of Branching Time", Proc. 8th ACM Syrup. on Principles of Programming Languages, Williamsburg, January 1981, pp. 164--176.

Digital Library

Google Scholar

[3]

E.M. Clarke, E.A., Emerson, A.P. Sistla, "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logics Specifications: A Practical Approach", Proc. lOth ACM Syrup. on Principles of Programming Languages, Austin, 1983, pp. 117-126.

Digital Library

Google Scholar

[4]

E.A. Emerson, E. M. Clarke, "Using Branching Time Logic to Synthesize Synchronization Skeletons", Science of Computer Programming, 2(1982), pp. 241-266.

Crossref

Google Scholar

[5]

E.A. Emerson, J.Y. Halpern,"Decision Procedures and Expressiveness in the Temporal Logic of Branching Time", J. Computer and System Sciences, 30(1985), pp. 1-34.

Digital Library

Google Scholar

[6]

E.A. Emerson, J.Y. Halpern, '"'Sometimes" and "Not Never" Revisited: On Branching vs. Linear Time", Proc. lOth ACM Syrup. on Principles of Programming Languages, Austin, 1983, pp. 127-140.

Digital Library

Google Scholar

[7]

E.A. Emerson, C.L. Lei, "Temporal Model Checking under Generalized Fairness Constralnts". Proc. 18th Hawaii Int'l Conference on System Sciences, 1985.

Google Scholar

[8]

E.A. Emerson, C.L. Lei, "Modalities for Model Checking: Branching Time Strikes Back", Pros. 12th ACM Syrup. on Principles of Programming Languages, New Orleans, 1985, pp. 84-96.

Digital Library

Google Scholar

[9]

E. A. Emerson, "Alternative Semantics for Temporal Logic", Theoretical Computer Science, 26(1983), pp. 120-130.

Crossref

Google Scholar

[10]

E. A. Emerson, "Automata, Tableau and Temporal Logic", in Logics of Programs, Lecture Notes in Computer Science, vol. 193, Springer-Verlag, Berlin, 1985, pp. 79-88.

Digital Library

Google Scholar

[11]

E.A. Emerson, A.P. Sistla,"Deciding Branching Time Logic", Information and Control, 61(1984), pp. 175-201.

Crossref

Google Scholar

[12]

N. Francez, D. Kozen, "Generalized Fair Termination", Pros. 11th ACM Syrup. on Principles of Programming Languages, Salt Lake City, 1983, pp. 46-53.

Digital Library

Google Scholar

[13]

D.M. Gabbay, "Investigation in Modal and Tense Logic" Reidel, 1976.

Google Scholar

[14]

D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, "The Temporal Analysis of Fairness", Pros. 7th ACM Syrup. on Principles of Programming Languages, Las Vegas, 1980, pp. 163-173.

Digital Library

Google Scholar

[15]

S. Hart, M. Sharir, "Probabilistic Temporal Logics for Finite and Bounded Models", Proc. 16th ACM Syrup. on Theory of Computing, Washington, 1984, pp. 1-13.

Digital Library

Google Scholar

[16]

N.D. Jones, W.T. Laaser, "Complete Problems in Deterministic Polynomial Time", Theoretical Computer Science 3(1977), pp. 105-117.

Crossref

Google Scholar

[17]

S. Krans, "The decision problem for TG' (in Hebrew), M.Se. Thesis, The Hebrew University in Jerusalem, 1984.

Google Scholar

[18]

J.G. Kemeny, J.L. Snell, A.W. Knapp, "Denumerable Markov Chains" D. van Nostrand Company, 1966.

Google Scholar

[19]

S. Kraus, D. Lehmann, "Decision Procedures for Time and Chance", Proc. 24th IEEE Syrup. on Foundations of Computer Science, Tucson, 1983, pp. 202-209.

Google Scholar

[20]

L. Lamport, "Sometimes is Sometimes Not Never", Proc. 7th ACM Symp. on Principles of Programming Languages, Las Vegas, January 1980, pp. 174--185.

Digital Library

Google Scholar

[21]

O. Lichtenstein, A. Pnueli, "Checking that Finite-State Concurrent Programs Satisfy Their Linear Specification", Proc. 12th ACM Syrup. on Principles of Programming Languages, New Orleans, 1985, pp. 97-107.

Digital Library

Google Scholar

[22]

D. Lehman, A. Pnueli, J. Stavi, "Impartiality, Justice, and Fairness: The Ethics of Concurrent Termination", Proc. 8th Int'l Colloq. on Automata, Languages, and Programming 1981, Lecture Notes in Computer Science - Vol. 115, Springer-Verlag, pp.264-277.

Digital Library

Google Scholar

[23]

D. Lehman, S. Shelah, "Reasoning with Time and Chance", Information and Control 53(1982), pp. 165.-198.

Crossref

Google Scholar

[24]

R. McNaughton, "Testing and Generating Infinite Sequences by a Finite Automaton", Information and Control 9 (1966), pp. 521-530

Crossref

Google Scholar

[25]

Z. Manna, P. Wolper, "Synthesis of Communicating Processes from Temporal Logic Specifications", ACM Trans. on Programming Languages and Systems, 6(1984), pp. 68-93.

Digital Library

Google Scholar

[26]

A. Pnueli, "The Temporal Logic of Programs", Proe. 8th IEEE Symp. on Foundations of Computer Science, Providence, 1977, pp. 46.-57.

Google Scholar

[27]

A. Pnueli, "The Temporal Logic of Concurrent Programs", Theoretical Computer Science 13(1980, pp. 45-60.

Google Scholar

[28]

A. Pnueli, "On the Extremely Fair Treatment of Probabilistic Algorithms", Proe. 15th ACM Syrup. on Theory of Computing, Boston, 1983, pp. 278-290.

Digital Library

Google Scholar

[29]

J.P. Queille, J. Sifakis, "Fairness and Related Properties in Transition Systems'; Research Report #292, IMA.G, Grenoble, 1982.

Google Scholar

[30]

M.O. Rabin, "Weakly Definable Relations and Special Automata", Proe. Symp. Math. Logic and Foundations of Set Theory (Y. Bar-Hillel, ed.), North-Holland, 1970, pp. 1-23.

Google Scholar

[31]

M.O. Rabin, "Automata on Infinite Objects and Church's Problem", Proe. Regional AMS Conf. Series in Math. 13(1972), pp. 1-22.

Google Scholar

[32]

M. O. Rabin, D. Scott, "Finite Automata and their Decision Problems", IBM J. Res. 6~ Dev., 3(1959), pp 114-125.

Digital Library

Google Scholar

[33]

R.S. Streett, "Propositional Dynamic Logic of Looping and Converse", Information and Control 54(1982), pp. 121-141.

Crossref

Google Scholar

[34]

M. Y. Vardi, L. Stockmeyer, "Improved Upper and Lower Bounds for Modal Logics of Programs", Proe. A CM 17th Symposium on Theory of Computing, Providence, May 1985, pp. 240-251.

Digital Library

Google Scholar

[35]

M. Y. Vardi, P. Wolper, "Automata Theoretic Techniques for Modal Logics of Programs", Proe. ACM Syrup. on Theory of Computing, Washington, April 1984, pp. 446.-456 (complete version to appear in J. Computer and System Sciences).

Digital Library

Google Scholar

[36]

P. Wolper, M. Y. Vardi, A. P. Sistla, "Reasoning about Infinite Computation Paths", Proc. 24th IEEE Syrup. on Foundations of Computer Science, Tucson, 1983, pp. 185-194.

Google Scholar

Cited By

View all

Aminof BDe Giacomo GRubin SZuleger F(2023)Stochastic Best-Effort Strategies for Borel Goals2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175747(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175747
Mccabe-Dansted JReynolds M(2017)To be fair, use bundlesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-017-9546-x80:3-4(317-364)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10472-017-9546-x
McCabe-Dansted JReynolds M(2014)Verification of Rewrite Rules for Computation Tree Logics2014 21st International Symposium on Temporal Representation and Reasoning10.1109/TIME.2014.25(142-151)Online publication date: Sep-2014
https://doi.org/10.1109/TIME.2014.25
Show More Cited By

Recommendations

Execution privatization for scheduler-oblivious concurrent programs
OOPSLA '12

Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious:...
Execution privatization for scheduler-oblivious concurrent programs
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious:...
Efficient Fair Secure Two-Party Computation
APSCC '12: Proceedings of the 2012 IEEE Asia-Pacific Services Computing Conference)

Yao first introduced a constant-round protocol for secure two-party computation (2PC) withstanding semi-honest adversaries by using a tool called """"garbled circuit"""". Later, many protocols based on garbled circuit approach have been presented, most ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

STOC '86: Proceedings of the eighteenth annual ACM symposium on Theory of computing

November 1986

461 pages

ISBN:0897911938

DOI:10.1145/12130

Chairman:
Juris Hartmanis

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 1986

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

STOC86

Sponsor:

SIGACT

STOC86: Eighteenth Annaul ACM Symposium on Theory of Computing

May 28 - 30, 1986

California, Berkeley, USA

Acceptance Rates

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

Upcoming Conference

STOC '25

Sponsor:
sigact

57th Annual ACM Symposium on Theory of Computing (STOC 2025)

June 23 - 27, 2025

Prague , Czech Republic

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
340
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)7

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Aminof BDe Giacomo GRubin SZuleger F(2023)Stochastic Best-Effort Strategies for Borel Goals2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175747(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175747
Mccabe-Dansted JReynolds M(2017)To be fair, use bundlesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-017-9546-x80:3-4(317-364)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10472-017-9546-x
McCabe-Dansted JReynolds M(2014)Verification of Rewrite Rules for Computation Tree Logics2014 21st International Symposium on Temporal Representation and Reasoning10.1109/TIME.2014.25(142-151)Online publication date: Sep-2014
https://doi.org/10.1109/TIME.2014.25
McCabe-Dansted JReynolds M(2014)Fairness with EXPTIME Bundled CTL Tableau2014 21st International Symposium on Temporal Representation and Reasoning10.1109/TIME.2014.22(164-173)Online publication date: Sep-2014
https://doi.org/10.1109/TIME.2014.22
Matsikoudis ELee E(2012)From Transitions to ExecutionsCoalgebraic Methods in Computer Science10.1007/978-3-642-32784-1_10(170-190)Online publication date: 2012
https://doi.org/10.1007/978-3-642-32784-1_10
Emerson ESrinivasan J(2005)Branching time temporal logicLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency10.1007/BFb0013022(123-172)Online publication date: 9-Jun-2005
https://doi.org/10.1007/BFb0013022
Emerson E(2005)Automated temporal reasoning about reactive systemsLogics for Concurrency10.1007/3-540-60915-6_3(41-101)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-60915-6_3
Stirling CWalker D(2005)CCS, liveness, and local model checking in the linear time mu-calculusAutomatic Verification Methods for Finite State Systems10.1007/3-540-52148-8_14(166-178)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-52148-8_14
Wolper P(2005)On the relation of programs and computations to models of temporal logicTemporal Logic in Specification10.1007/3-540-51803-7_23(75-123)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-51803-7_23
Katz SPeled D(2005)Interleaving set temporal logicTemporal Logic in Specification10.1007/3-540-51803-7_20(21-43)Online publication date: 25-May-2005
https://doi.org/10.1007/3-540-51803-7_20
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

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Execution privatization for scheduler-oblivious concurrent programs

Execution privatization for scheduler-oblivious concurrent programs

Efficient Fair Secure Two-Party Computation