article

Free access

An automata-theoretic approach to branching-time model checking

Authors:

Orna Kupferman,

Moshe Y. Vardi,

Pierre WolperAuthors Info & Claims

Journal of the ACM (JACM), Volume 47, Issue 2

Pages 312 - 360

https://doi.org/10.1145/333979.333987

Published: 01 March 2000 Publication History

Abstract

Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper, we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only can they be used to obtain optimal decision procedures, as was shown by Muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.

References

[1]

ALUR, R., HENZINGER, T. A., AND KUPFERMAN, 0. 1997. Alternating-time temporal logic. In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 100-109.]]

[2]

ANDERSEN, H. R., AND VERGAUWEN, B. 1995. Efficient checking of behavioural relations and modal assertions using fixed-point inversion. In Computer Aided Verification, Proceedings of the 7th International Conference (Liege, Belgium, July). Lecture Notes in Computer Science, vol. 939. Springer-Verlag, New York, pp. 142-154.]]

[3]

ANDERSON, H. R. 1992. Model checking and boolean graphs. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 582. Springer- Verlag, New York, pp. 1-19.]]

[4]

BANIEQBAL, B., AND BARRINGER, H. 1987. Temporal logic with fixed points. In Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, vol. 398. Springer-Verlag, New York, pp. 62-74.]]

[5]

BEERI, C. 1980. On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Datab. Syst. 5, 3 (Sept.), 241-259.]]

[6]

BEERI, C., AND BERNSTEIN, P.A. 1979. Computational problems related to the design of normal form relational schemas. ACM Trans. Datab. Syst. 4, 1 (Mar.), 30-59.]]

[7]

BERNHOLTZ, 0., AND GRUMBERG, 0. 1993. Branching time temporal logic and amorphous tree automata. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 262-277.]]

[8]

BHAT, G., AND CLEAVELAND, R. 1996a. Efficient local model-checking for fragments of the modal /x-calculus. In Proceedings of the 1996 Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes on Computer Science, vol. 1055. Springer-Verlag, Berlin, Germany.]]

[9]

BHAT, G., AND CLEAVELAND, R. 1996b. Efficient model checking via the equational/x-calculus. In Proceedings of the llth IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 304-312.]]

[10]

CHANDRA, A. K., KOZEN, D. C., AND STOCKMEYER, L.J. 1981. Alternation. J. ACM 28, 1 (Jan.), 114-133.]]

[11]

CLARKE, E. M., EMERSON, E. A., AND SISTLA, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Syst. 8, 2 (Apr.), 244-263.]]

[12]

CLARKE, E. M., GRUMBERG, 0., AND LONG, D. 1993. Verification tools for finite-state concurrent systems. In Decade of Concurrency--Reflections and Perspectives (Proceedings of REX School) J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Eds. Lecture Notes in Computer Science, vol. 803. Springer-Verlag, New York, pp. 124-175.]]

[13]

CLEAVELAND, R. 1993. A linear-time model-checking algorithm for the alternation-free modal /x-calculus. Form. Meth. Syst. Des. 2, 121-147.]]

[14]

COURCOUBETIS, C., VARDI, M. Y., WOLPER, P., AND YANNAKAKIS, M. 1992. Memory efficient algorithms for the verification of temporal properties. Form. Meth. Syst. Des. 1,275-288.]]

[15]

DOWLING, W. F., AND GALLIER, J.H. 1984. Linear-time algorithms for testing the satisfiability of propositional horn formulae. J. Logic Prog. 1, 3, 267-284.]]

[16]

EMERSON, E.A. 1985. Automata, tableaux, and temporal logics. In Proceedings of the Workshop on Logic of Programs. Lecture Notes in Computer Science, vol. 193. Springer-Verlag, New York, pp. 79-87.]]

[17]

EMERSON, E.A. 1996. Automated temporal reasoning about reactive systems. In Proceedings of the VIII-th BANFF Higher Order Workshop. Lecture Notes in Computer Science, vol. 1043. Springer- Verlag, New York, pp. 41-101.]]

[18]

EMERSON, E. A., AND HALPERN, J.Y. 1986. "Sometimes" and "not never" revisited: On branching versus linear time temporal logic. J. ACM 33, 1 (Jan.), 151-178.]]

[19]

EMERSON, E. A., AND JUTLA, C. 1988. The complexity of tree automata and logics of programs. In Proceedings of the 29th IEEE Symposium on Foundations of Computer Science (White Plains, N.Y., Oct.) IEEE Computer Society Press, Los Alamitos, Calif., pp. 328-337.]]

[20]

EMERSON, E. A., AND JUTLA, C. 1991. Tree automata, Mu-calculus and determinacy. In Proceedings of the 32nd IEEE Symposium on Foundations of Computer Science (San Juan, P.R., Oct.). IEEE Computer Society Press, Los Alamitos, Calif., pp. 368-377.]]

[21]

EMERSON, E. A., JUTLA, C., AND SISTLA, A. P. 1993. On model-checking for fragments of /x-calculus. In Computer Aided Verification, Proceedings of the 5th International Conference (Elounda, Crete, June). Lecture Notes in Computer Science, vol. 697. Springer-Verlag, New York, pp. 385-396.]]

[22]

EMERSON, E. A., AND LEI, C.-L. 1986. Efficient model checking in fragments of the propositional /x-calculus. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June). pp. 267-278.]]

[23]

EMERSON, E. A., AND SISTLA, A.P. 1984. Deciding branching time logic. In Proceedings of the 16th Annual ACM Symposium on Theory of Computing (Washington, D.C., Apr. 30-May 2). ACM, New York, pp. 14-24.]]

[24]

FISCHER, M. J., AND LADNER, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194-211.]]

[25]

GRAEDEL, E., AND WALUKIEWICZ, I. 1999. Guarded fixed point logic. In Proceedings of the 14th Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif.]]

[26]

GREENLAW, R., HOOVER, H. J., AND RUZZO, W.L. 1995. Limits of parallel computation. Oxford University Press, Oxford, England.]]

[27]

HENZINGER, T. A., KUPFERMAN, 0., AND VARDI, M.Y. 1996. A space-efficient on-the-fly algorithm for real-time model checking. In Proceedings of the 7th Conference on Concurrency Theory (Pisa, Italy, Aug.). Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, New York, pp. 514-529.]]

[28]

IMMERMAN, N. 1981. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 3, 384-406.]]

[29]

JARD, C., AND JERON, T. 1989. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proceedings of the International Workshop (Grenoble, Switzerland, June). Lecture Notes in Computer Science, vol. 407. Springer- Verlag, New York, pp. 189-196.]]

[30]

JONES, N. D. 1975. Space-bounded reducibility among combinatorial problems. J. Comput. Syst. Sci. 11, 68-75.]]

[31]

JUTLA, C.S. 1990. Automata on infinite objects and modal logics of programs. Ph.D. dissertation, Univ. Texas, Austin, Texas.]]

[32]

KOZEN, D. 1977. Lower bounds for natural proof systems. In Proceedings of the 18th IEEE Symposium on Foundation of Computer Science. IEEE Computer Science Press, Los Alamitos, Calif., pp. 254-266.]]

[33]

KOZEN, D. 1983. Results on the propositional/x-calculus. Theoret. Comput. Sci. 27, 333-354.]]

[34]

KUPFERMAN, 0., AND VARDI, M. Y. 1995. On the complexity of branching modular model checking. In Proceedings of the 6th Conference on Concurrency Theory (Philadelphia, Pa., Aug.). Lecture Notes in Computer Science, vol. 962. Springer-Verlag, New York, pp. 408-422.]]

[35]

KUPFERMAN, 0., AND VARDI, M. Y. 1996. Module checking. In Computer Aided Verification, Proceedings of the 8th International Conference. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, New York, pp. 75-86.]]

[36]

KUPFERMAN, 0., AND VARDI, M.Y. 1997. Module checking revisited. In Computer Aided Verification, Proceedings of the 9th International Conference. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, New York, pp. 36-47.]]

[37]

KUPFERMAN, 0., AND VARDI, M.Y. 1998a. Freedom, weakness, and determinism: From lineartime to branching-time. In Proceedings of the 13th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 81-92.]]

[38]

KUPFERMAN, 0., AND VARDI, M. Y. 1998b. Modular model checking. In Proceedings of the Compositionality Workshop. Lecture Notes in Computer Science, vol. 1536. Springer-Verlag, New York, pp. 381-401.]]

[39]

KUPFERMAN, 0., AND VARDI, M. Y. 1998c. Weak alternating automata and tree automata emptiness. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing (Dallas, Tex., May 23-26). ACM, New York, pp. 224-233.]]

[40]

KUPFERMAN, 0., AND VARDI, M. Y. 1999a. Church's problem revisited. Bull. Symb. Logic 5, 2, 245-263.]]

[41]

KUPFERMAN, 0., AND VARDI, M. Y. 1999b. Robust satisfaction. In Proceedings of the lOth Conference on Concurrency Theory. Lecture Notes in Computer Science. Springer-Verlag, New York.]]

[42]

KUPFERMAN, 0., VARDI, M. Y., AND WOLPER, P. 1997. Module checking. Inf. Comput. to appear.]]

[43]

LAMPORT, L. 1980. Sometimes is sometimes "not never"--On the temporal logic of programs. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, ACM, New York, pp. 174-185.]]

[44]

LARSEN, K.G. 1992. Efficient local correctness checking. In Proceedings of the 4th Conference on Computer Aided Verification (Montreal, Que., Canada, June). Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 30-43.]]

[45]

LICHTENSTEIN, 0., AND PNUELI, A. 1985. Checking that finite state concurrent programs satisfy their linear specification. In Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages (New Orleans, La., Jan.) ACM, New York, pp. 97-107.]]

[46]

LYNCH, N. 1977. Log space recognition and translation of parenthesis languages. J. ACM 24, 4 (Oct.), 583-590.]]

[47]

MIHAIL, M., AND PAPADEMITRIOU, C.H. 1994. On the random walk method for protocol testing. In Proceedings of the 5th Annual Conference on Computer Aided Verification (Stanford, Calif., June). Lecture Notes in Computer Science, vol. 818. Springer-Verlag, New York, pp. 132-141.]]

[48]

MIYANO, S., AND HAYASHI, T. 1984. Alternating finite automata on ~0-words. Theoret. Comput. Sci. 32, 321-330.]]

[49]

MULLER, D. E., SAOUDI, A., AND SCHUPP, P.E. 1986. Alternating automata, the weak monadic theory of the tree and its complexity. In Proceedings of the 13th International Colloquium on Automata, Languages and Programming. Springer-Verlag, New York.]]

[50]

MULLER, D. E., SAOUDI, A., AND SCHUPP, P.E. 1988. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science (Edinburgh, Scotland, July). IEEE Computer Society Press, Los Alamitos, Calif., pp. 422-427.]]

[51]

MULLER, D. E., AND SCHUPP, P.E. 1987. Alternating automata on infinite trees. Theoret. Comput. Sci. 54, 267-276.]]

[52]

PNUELI, A. 1981. The temporal semantics of concurrent programs. Theoret. Comput. Sci. 13, 45-60.]]

[53]

QUEILLE, J. P., AND SIFAKIS, J. 1981. Specification and verification of concurrent systems in Cesar. In Proceedings of the 5th International Symposium on Programming. Lecture Notes in Computer Science, vol. 137. Springer-Verlag, New York, pp. 337-351.]]

[54]

RABIN, M.O. 1969. Decidability of second order theories and automata on infinite trees. Trans. AMS 141, 1-35.]]

[55]

RABIN, M. O. 1970. Weakly definable relations and special automata. In Proceedings of the Symposium on Mathematical Logic and Foundations of Set Theory. North Holland, Amsterdam, New York, pp. 1-23.]]

[56]

SAVITCH, W.J. 1970. Relationship between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177-192.]]

[57]

SLUTZKI, G. 1985. Alternating tree automata. Theoret. Comput. Sci. 41, 305-318.]]

[58]

STIRLING, C. 1996. Games and modal mu-calculus. In Proceedings of the 13th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science, vol. 1055. Springer- Verlag, New York, pp. 298-312.]]

[59]

STIRLING, C., AND WALKER, D. 1991. Local model checking in the modal Mu-calculus. Theoret. Comput. Sci. 89, 1, 161-177.]]

[60]

STREET, R. S., AND EMERSON, E.A. 1984. An elementary decision procedure for the/x-calculus. In Proceedings of the llth International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 172. Springer-Verlag, New York, pp. 465-472.]]

[61]

TARJAN, R. E. 1972. Depth first search and linear graph algorithms. SIAM J. Comput. 1, 2, 146-160.]]

[62]

THOMAS, W. 1990. Automata on infinite objects. Handb. Theoret. Comput. Sci., 165-191.]]

[63]

VARDI, M. Y. 1982. The complexity of relational query languages. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing (San Francisco, Calif., May 5-7). ACM, New York, pp. 137-146.]]

[64]

VARDI, M. Y. 1995. On the complexity of modular model checking. In Proceedings of the 10th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., pp. 101-111.]]

[65]

VARDI, M. Y., AND STOCKMEYER, L. 1985. Improved upper and lower bounds for modal logics of programs. In Proceedings of the 17th Annual ACM Symposium on Theory of Computing (Providence, R.I., May 6-8). ACM, New York, pp. 240-251.]]

[66]

VARDI, M. Y., AND WOLPER, P. 1984. Yet another process logic. In Logics of Programs. Lecture Notes in Computer Science, vol. 164. Springer-Verlag, New York, pp. 501-512.]]

[67]

VARDI, M. Y., AND WOLPER, P. 1986a. An automata-theoretic approach to automatic program verification. In Proceedings of the 1st Symposium on Logic in Computer Science (Cambridge, Mass., June). pp. 322-331.]]

[68]

VARDI, M. Y., AND WOLPER, P. 1986b. Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32, 2 (Apr.), 182-221.]]

[69]

VARDI, M. Y., AND WOLPER, P. 1994. Reasoning about infinite computations. Inf. Comput. 115, 1 (Nov.), 1-37.]]

[70]

VERGAUWEN, B., AND LEWIS, J. 1993. A linear local model checking algorithm for CTL. In Proceedings of the 4th Conference on Concurrency Theory (Hildesheim, Aug.). Lecture Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 447-461.]]

[71]

VISSER, W. 1998. Efficient CTL* model checking using games and automata. Ph.D. dissertation. Manchester University.]]

[72]

VISSER, W., AND BARRINGER, H. 1999. CTL* model checking for SPIN. In Software Tools for Technology Transfer. Lecture Notes in Computer Science, Springer-Verlag, New York.]]

[73]

WILLEMS, B., AND WOLPER, P. 1996. Partial-order methods for model checking: From linear time to branching time. In Proceedings of the l lth Annual Symposium on Logic in Computer Science. (New Brunswick, N.J., July).]]

[74]

WOLPER, P. 1983. Temporal logic can be more expressive. Inf. Control, 56, 1-2, 72-99.]]

[75]

WOLPER, P. 1989. On the relation of programs and computations to models of temporal logic. In Proceedings of the Temporal Logic in Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, Springer-Verlag, New York, pp. 75-123.]]

Cited By

Jamroga WMittelmann MMurano APerelli GDastani MSichman JAlechina NDignum V(2024)Playing Quantitative Games Against an Authority: On the Module Checking ProblemProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662947(926-934)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662947
Carvalho LDegiovanni RCordy MAguirre NLe Traon YPapadakis MRoychoudhury APaiva AAbreu RStorey M(2024)SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639087(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639087
Alwhishi GBentahar JElwhishi APedrycz W(2024)Multi-valued verification of commitment systems with uncertainty and inconsistency in multi-source data settingsInformation Fusion10.1016/j.inffus.2024.102502111:COnline publication date: 1-Nov-2024
https://dl.acm.org/doi/10.1016/j.inffus.2024.102502
Show More Cited By

Index Terms

An automata-theoretic approach to branching-time model checking
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
      1. Temporal reasoning
2. Theory of computation
  1. Formal languages and automata theory
  2. Logic
    1. Modal and temporal logics

Recommendations

Branching-Time Model-Checking of Probabilistic Pushdown Automata

In this paper we study complexity of the model-checking problem for probabilistic pushdown automata (pPDA) and qualitative fragments of two branching-time logics PCTL* and PECTL*. We prove tha this problem is in 2-EXPTIME for pPDA and qualitative PCTL*. ...
Branching-time model-checking of probabilistic pushdown automata

In this paper we study the model-checking problem for probabilistic pushdown automata (pPDA) and branching-time probabilistic logics PCTL and PCTL^@?. We show that model-checking pPDA against general PCTL formulae is undecidable, but we yield positive ...
An automata-theoretic approach to modular model checking

In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 47, Issue 2

March 2000

192 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/333979

Issue’s Table of Contents

Copyright © 2000 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 2000

Published in JACM Volume 47, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

412
Total Citations
View Citations
2,381
Total Downloads

Downloads (Last 12 months)126
Downloads (Last 6 weeks)14

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jamroga WMittelmann MMurano APerelli GDastani MSichman JAlechina NDignum V(2024)Playing Quantitative Games Against an Authority: On the Module Checking ProblemProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3662947(926-934)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3662947
Carvalho LDegiovanni RCordy MAguirre NLe Traon YPapadakis MRoychoudhury APaiva AAbreu RStorey M(2024)SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639087(1-13)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639087
Alwhishi GBentahar JElwhishi APedrycz W(2024)Multi-valued verification of commitment systems with uncertainty and inconsistency in multi-source data settingsInformation Fusion10.1016/j.inffus.2024.102502111:COnline publication date: 1-Nov-2024
https://dl.acm.org/doi/10.1016/j.inffus.2024.102502
Alwhishi GBentahar JElwhishi APedrycz WDrawel N(2024)Multi-valued model checking IoT and intelligent systems with commitment protocols in multi-source data environmentsInformation Fusion10.1016/j.inffus.2023.102048102:COnline publication date: 1-Feb-2024
https://dl.acm.org/doi/10.1016/j.inffus.2023.102048
Alwhishi GBentahar JElwhishi APedrycz W(2024)MV-Checker: A software tool for multi-valued model checking intelligent applications with trust and commitmentExpert Systems with Applications10.1016/j.eswa.2023.123113245(123113)Online publication date: Jul-2024
https://doi.org/10.1016/j.eswa.2023.123113
Catta DLeneutre JMalvone V(2023)Attack Graphs & Subset Sabotage GamesIntelligenza Artificiale10.3233/IA-22108017:1(77-88)Online publication date: 7-Jun-2023
https://doi.org/10.3233/IA-221080
Mittelmann MMurano APerrussel LElkind E(2023)Discounting in strategy logicProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/26(225-233)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/26
Bouyer PKupferman OMarkey NMaubert BMurano APerelli G(2023)Reasoning about Quality and Fuzziness of Strategic BehaviorsACM Transactions on Computational Logic10.1145/358249824:3(1-38)Online publication date: 7-Apr-2023
https://dl.acm.org/doi/10.1145/3582498
Sekiyama TUnno H(2023)Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited ContinuationsProceedings of the ACM on Programming Languages10.1145/35712647:POPL(2079-2110)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571264
Benerecetti MMogavero FPeron A(2023)Taming Strategy Logic: Non-Recurrent FragmentsInformation and Computation10.1016/j.ic.2023.105081294(105081)Online publication date: Oct-2023
https://doi.org/10.1016/j.ic.2023.105081
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents