{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:15:01Z","timestamp":1794348901364,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540746201","type":"print"},{"value":"9783540746218","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74621-8_11","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T07:46:32Z","timestamp":1187768792000},"page":"163-177","source":"Crossref","is-referenced-by-count":8,"title":["Temporal Logic with Capacity Constraints"],"prefix":"10.1007","author":[{"given":"Clare","family":"Dixon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional Satisfiability and Constraint Programming: A Comparative Survey. ACM Computing Surveys\u00a038(4) (2006)","DOI":"10.1145\/1177352.1177354"},{"key":"11_CR2","unstructured":"Chen, B.: Parallel Scheduling for Early Completion. In: Leung, J.Y.-T. (ed.) Handbook of Scheduling: Algorithms, Models, and Performance Analysis, ch. 9, Chapman & Hall\/CRC Press (2004)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Computer Aided Verification","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 249\u2013260. Springer, Heidelberg (1999)"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1023\/A:1018930406487","volume":"70","author":"S. Dauz\u00e9re-P\u00e9r\u00e8s","year":"1997","unstructured":"Dauz\u00e9re-P\u00e9r\u00e8s, S., Paulli, J.: An Integrated Approach for Modeling and Solving the General Multiprocessor Job-shop Scheduling Problem using Tabu Search. Annals of Operations Research\u00a070, 281\u2013306 (1997)","journal-title":"Annals of Operations Research"},{"key":"11_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-45616-3_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Degtyarev","year":"2002","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 85\u201399. Springer, Heidelberg (2002)"},{"issue":"1","key":"11_CR6","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.2001.3094","volume":"174","author":"S. Demri","year":"2002","unstructured":"Demri, S., Schnoebelen, P.: The Complexity of Propositional Linear Temporal Logic in Simple Cases. Information and Computation\u00a0174(1), 84\u2013103 (2002)","journal-title":"Information and Computation"},{"key":"11_CR7","volume-title":"Proc. Thirteenth International Symposium on Temporal Representation and Reasoning (TIME)","author":"C. Dixon","year":"2006","unstructured":"Dixon, C., Fisher, M., Konev, B.: Is There a Future for Deductive Temporal Verification? In: Proc. Thirteenth International Symposium on Temporal Representation and Reasoning (TIME), IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"11_CR8","volume-title":"Proc. International Joint Conference on Artificial Intelligence (IJCAI)","author":"C. Dixon","year":"2007","unstructured":"Dixon, C., Fisher, M., Konev, B.: Tractable Temporal Reasoning. In: Proc. International Joint Conference on Artificial Intelligence (IJCAI), AAAI Press, Stanford, California (2007)"},{"key":"11_CR9","first-page":"996","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996\u20131072. Elsevier, Amsterdam (1990)"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: Basic Models","author":"J. Esparza","year":"1998","unstructured":"Esparza, J.: Decidability and Complexity of Petri Net Problems - An Introduction. In: Reisig, W., Rozenberg, G. (eds.) Lectures on Petri Nets I: Basic Models. LNCS, vol.\u00a01491, pp. 374\u2013428. Springer, Heidelberg (1998)"},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal Temporal Resolution. ACM Transactions on Computational Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: The Temporal Analysis of Fairness. In: Proc. Seventh ACM Symposium on the Principles of Programming Languages (POPL), pp. 163\u2013173 (January 1980)","DOI":"10.1145\/567446.567462"},{"issue":"3","key":"11_CR13","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-005-7354-1","volume":"34","author":"M.-C.F. Gago","year":"2005","unstructured":"Gago, M.-C.F., Hustadt, U., Dixon, C., Fisher, M., Konev, B.: First-Order Temporal Verification in Practice. Journal of Automated Reasoning\u00a034(3), 295\u2013321 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2002","author":"D. Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to B\u00fcchi Automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol.\u00a02529, pp. 308\u2013326. Springer, Heidelberg (2002)"},{"key":"11_CR15","unstructured":"Gough, G.D.: Decision Procedures for Temporal Logic. Master\u2019s thesis, Department of Computer Science, University of Manchester, October, Also University of Manchester, Department of Computer Science, Technical Report UMCS-89-10-1 (1984)"},{"key":"11_CR16","unstructured":"Jaeger, G., Balsiger, P., Heuerding, A., Schwendimann, S., Bianchi, M., Guggisberg, K., Janssen, G., Heinle, W., Achermann, F., Boroumand, A.D., Brambilla, P., Bucher, I., Zimmermann, H.: LWB\u2013The Logics Workbench 1.1. University of Berne, Switzerland (2002), \n                    \n                      http:\/\/www.lwb.unibe.ch"},{"key":"11_CR17","unstructured":"Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis, Eindhoven University of Technology, Eindhoven, The Netherlands (1999)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-48068-4_14","volume-title":"Application and Theory of Petri Nets 2002","author":"E. Kindler","year":"2002","unstructured":"Kindler, E.: Petri Nets, Situations, and Automata. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol.\u00a02360, pp. 217\u2013236. Springer, Heidelberg (2002)"},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/BF01211299","volume":"9","author":"E. Kindler","year":"1997","unstructured":"Kindler, E., Reisig, W., V\u00f6lzer, H., Walter, R.: Petri Net Based Verification of Distributed Algorithms: An Example. Formal Aspects of Computing\u00a09(4), 409\u2013424 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR20","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"L. Lamport","year":"2003","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley Professional, Reading (2003)"},{"key":"11_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"11_CR22","unstructured":"Schwendimann, S.: Aspects of Computational Logic. PhD thesis, University of Bern, Switzerland (1998)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/11513988_35","volume-title":"Computer Aided Verification","author":"R. Sebastiani","year":"2005","unstructured":"Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 350\u2013363. Springer, Heidelberg (2005)"},{"key":"11_CR24","unstructured":"Wolper, P.: The Tableau Method for Temporal Logic: An Overview. Logique et Analyse, 110\u2013111,119\u2013136, (June-September 1985)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:30:39Z","timestamp":1619505039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746201","9783540746218"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_11","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}