{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:57:08Z","timestamp":1762459028164,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642332951"},{"type":"electronic","value":"9783642332968"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33296-8_12","type":"book-chapter","created":{"date-parts":[[2012,9,17]],"date-time":"2012-09-17T02:24:55Z","timestamp":1347848695000},"page":"147-162","source":"Crossref","is-referenced-by-count":5,"title":["Specifying and Verifying Declarative Fluent Temporal Logic Properties of Workflows"],"prefix":"10.1007","author":[{"given":"Germ\u00e1n","family":"Regis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicol\u00e1s","family":"Ricci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nazareno M.","family":"Aguirre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Maibaum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1022883727209","volume":"14","author":"W.M.P. Aalst van der","year":"2003","unstructured":"van der Aalst, W.M.P., ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow Patterns. Distributed and Parallel Databases\u00a014, 5\u201351 (2003)","journal-title":"Distributed and Parallel Databases"},{"key":"12_CR2","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/j.is.2004.02.002","volume":"30","author":"W.M.P. Aalst","year":"2005","unstructured":"van der Aalst, W.M.P., ter Hofstede, A.H.M.: YAWL: yet another workflow language. Inf. Syst. 30, 245\u2013275 (2005)","journal-title":"Inf. Syst."},{"issue":"3","key":"12_CR3","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s00165-010-0161-4","volume":"23","author":"W.M.P. Aalst van der","year":"2011","unstructured":"van der Aalst, W.M.P., et al.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput.\u00a023(3), 333\u2013363 (2011)","journal-title":"Formal Asp. Comput."},{"key":"12_CR4","unstructured":"van Breugel, F., Koshkina, M.: Models and Verification of BPEL (2006), http:\/\/www.cse.yorku.ca\/~franck\/research\/drafts\/tutorial.pdf"},{"key":"12_CR5","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (2000)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Rabbi, F., Wang, H., MacCaull, W.: YAWL2DVE: An Automated Translator for Workflow Verification. In: SSIRI, pp. 53\u201359 (2010)","DOI":"10.1109\/SSIRI.2010.31"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: ESEC \/ SIGSOFT FSE, pp. 257\u2013266 (2003)","DOI":"10.1145\/949952.940106"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Girault, C., Valk, R.: Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications. Springer (2002)","DOI":"10.1007\/978-3-662-05324-9"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"ter Hofstede, A.H.M., van der Aalst, W.M.P., Adams, M., Russell, N.: Modern Bussiness Process Automation. Springer (2010)","DOI":"10.1007\/978-3-642-03121-2"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Karamanolis, C.T., Giannakopoulou, D., Magee, J., Wheater, S.M.: Model Checking of Workflow Schemas. In: EDOC, pp. 170\u2013181 (2000)","DOI":"10.1109\/EDOC.2000.882357"},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.datak.2005.02.005","volume":"56","author":"E. Kindler","year":"2006","unstructured":"Kindler, E.: On the semantics of EPCs: Resolving the vicious circle. Data Knowl. Eng.\u00a056(1), 23\u201340 (2006)","journal-title":"Data Knowl. Eng."},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Leyla, N., Mashiyat, A.S., Wang, H., MacCaull, W.: Towards workflow verification. In: CASCON, pp. 253\u2013267 (2010)","DOI":"10.1145\/1923947.1923974"},{"key":"12_CR13","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. John Wiley & Sons (1999)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-23059-2_13","volume-title":"Business Process Management","author":"F.M. Maggi","year":"2011","unstructured":"Maggi, F.M., Montali, M., Westergaard, M., van der Aalst, W.M.P.: Monitoring Business Constraints with Linear Temporal Logic: An Approach Based on Colored Automata. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol.\u00a06896, pp. 132\u2013147. Springer, Heidelberg (2011)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer (1991)","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems -Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"16","key":"12_CR17","first-page":"1","volume":"4","author":"R. Miller","year":"1999","unstructured":"Miller, R., Shanahan, M.: The Event Calculus in Classical Logic - Alternative Axiomatisations. Linkoping Electronic Articles in Computer and Information Science\u00a04(16), 1\u201327 (1999)","journal-title":"Linkoping Electronic Articles in Computer and Information Science"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Morimoto, S.: A Survey of Formal Verification for Business Process Modeling. In: ICCS 2008, pp. 514\u2013522 (2008)","DOI":"10.1007\/978-3-540-69387-1_58"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: Declarative Workflow. In: Modern Business Process Automation, pp. 175\u2013201 (2010)","DOI":"10.1007\/978-3-642-03121-2_6"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-10373-5_38","volume-title":"Formal Methods and Software Engineering","author":"G. Regis","year":"2009","unstructured":"Regis, G., Aguirre, N., Maibaum, T.: Specifying and Verifying Business Processes Using PPML. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 737\u2013756. Springer, Heidelberg (2009)"},{"issue":"10","key":"12_CR21","doi-asserted-by":"publisher","first-page":"942","DOI":"10.1016\/j.scico.2010.09.007","volume":"76","author":"P.Y.H. Wong","year":"2011","unstructured":"Wong, P.Y.H., Gibbons, J.: Property specifications for workflow modelling. Sci. Comput. Program\u00a076(10), 942\u2013967 (2011)","journal-title":"Sci. Comput. Program"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33296-8_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T22:37:20Z","timestamp":1744151840000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33296-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642332951","9783642332968"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33296-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}