{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T17:12:47Z","timestamp":1649178767756},"reference-count":62,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":5319,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1999,1]]},"DOI":"10.1016\/s0004-3702(98)00104-0","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T14:46:00Z","timestamp":1027608360000},"page":"63-98","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning about nondeterministic and concurrent actions: A process algebra approach"],"prefix":"10.1016","volume":"107","author":[{"given":"Xiao Jun","family":"Chen","sequence":"first","affiliation":[]},{"given":"Giuseppe","family":"De Giacomo","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0004-3702(98)00104-0_BIB1","series-title":"Foundations of Databases","author":"Abiteboul","year":"1995"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB2","series-title":"Proc. 13th International Joint Conference on Artificial Intelligence (IJCAI-93)","first-page":"866","article-title":"Representing concurrent actions in extended logic programming","author":"Baral","year":"1993"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB3","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","article-title":"Process algebra for synchronous communication","volume":"60","author":"Bergstra","year":"1984","journal-title":"Inform. and Control"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB4","series-title":"Proc. 5th International Conference on Database Theory (ICDT-95)","article-title":"Concurrency and communication in transaction logic","author":"Bonner","year":"1995"},{"issue":"3","key":"10.1016\/S0004-3702(98)00104-0_BIB5","first-page":"355","article-title":"Representing concurrent actions and solving conflicts, Journal of the Interest Group in Pure and Applied Logics (IGPL)","volume":"4","author":"Bornscheuer","year":"1996","journal-title":"Special issue of the ESPRIT project MEDLAR"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB6","series-title":"Proc. Workshop on Automatic Verification Methods for Finite State Systems","article-title":"Process calculi, from theory to practice: Verification tools","volume":"Vol. 407","author":"Boudol","year":"1990"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB7","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(92)90276-L","article-title":"Graphical versus logical specifications","volume":"106","author":"Boudol","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB8","series-title":"Proc. 12th International Joint Conference on Artificial Intelligence (IJCAI-91)","first-page":"274","article-title":"Complexity results for planning","author":"Bylander","year":"1991"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB9","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","article-title":"Tableaux-based model checking in the propositional mu-calculus","volume":"27","author":"Cleaveland","year":"1990","journal-title":"Acta Informatica"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB10","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","article-title":"The concurrency workbench: A semantics-based tool for the verification of concurrent systems","volume":"15","author":"Cleaveland","year":"1993","journal-title":"ACM Trans. Programming Languages Syst."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB11","series-title":"Computer-Aided Verification (CAV-96)","first-page":"394","article-title":"The NCSU concurrency workbench","volume":"Vol. 1102","author":"Cleaveland","year":"1996"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB12","series-title":"Proc. Colloquium on Trees and Algebra in Programming","first-page":"145","article-title":"CTL\u2217 and ECTL\u2217 as fragments of the modal mu-calculus","volume":"Vol. 581","author":"Dam","year":"1992"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB13","series-title":"Proc. 12th National Conference on Artificial Intelligence (AAAI-94)","first-page":"205","article-title":"Boosting the correspondence between description logics and propositional dynamic logics","author":"De Giacomo","year":"1994"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB14","series-title":"Proc. 15th International Joint Conference on Artificial Intelligence (IJCA1-97)","article-title":"Reasoning about concurrent executions, prioritized interrupts, and exogenous action in the situation calculus","author":"De Giacomo","year":"1997"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB15","series-title":"Proc. 6th International Conference on Principles of Knowledge Representation and Reasoning (KR'98)","article-title":"Execution monitoring of high-level robot programs","author":"De Giacomo","year":"1998"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB16","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00264365","article-title":"Extentional equivalences for transition system","volume":"24","author":"De Nicola","year":"1987","journal-title":"Acta Informatica"},{"issue":"1","key":"10.1016\/S0004-3702(98)00104-0_BIB17","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"\u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching time versus linear time temporal logic","volume":"33","author":"Emerson","year":"1986","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB18","volume":"Vol. B","author":"Emerson","year":"1990"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB19","series-title":"Logics for Concurrency: Structure versus Automata","first-page":"41","article-title":"Automated temporal reasoning about reactive systems","volume":"Vol. 1043","author":"Emerson","year":"1996"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB20","series-title":"Proc. 20th Annual Symposium on the Foundations of Computer Science","first-page":"328","article-title":"The complexity of tree automata and logics of programs","author":"Emerson","year":"1988"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB21","series-title":"Proc. 5th International Conference of Computer-Aided Verification","first-page":"385","article-title":"On model checking for fragments of the mu-calculus","volume":"Vol. 697","author":"Emerson","year":"1993"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB22","series-title":"Proc. 1st IEEE Symposium on Logics in Computer Science (LICS'86)","first-page":"267","article-title":"Efficient model checking in fragments of the mu-calculus","author":"Emerson","year":"1986"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB23","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/0743-1066(93)90035-F","article-title":"Representing action and change by logic programs","volume":"17","author":"Gelfond","year":"1993","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB24","series-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","first-page":"167","article-title":"What are the limitations of the situation calculus?","author":"Gelfond","year":"1991"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB25","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/S0019-9958(86)80031-6","article-title":"A model characterization of observational congruence on finite terms of CCS","volume":"68","author":"Graf","year":"1986","journal-title":"Inform. and Control"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB26","series-title":"Semantics with Applications","author":"Nielson","year":"1992"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB27","series-title":"Artificial Intelligence and Mathematical Theory of Computation\u2014Papers in Honor of John McCarthy","first-page":"151","article-title":"Model checking vs. theorem proving: A manifesto","author":"Halpern","year":"1991"},{"issue":"1","key":"10.1016\/S0004-3702(98)00104-0_BIB28","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","article-title":"Algebraic laws for nondeterminism and concurrency","volume":"32","author":"Hennessy","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB29","series-title":"Logics for Concurrency: Structure versus Automata","first-page":"102","article-title":"Decidability results in automata and process theory","volume":"Vol. 1043","author":"Hirishfeld","year":"1996"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB30","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB31","series-title":"Proc. 2nd International Conference on the Principles of Knowledge Representation and Reasoning (KR-91)","first-page":"387","article-title":"On the difference between updating a knowledge base and revising it","author":"Katsuno","year":"1991"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB32","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional mu-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB33","series-title":"Proc. 2nd Workshop on Logic of Programs","first-page":"313","article-title":"A decision procedure for the propositional mu-calculus","volume":"Vol. 164","author":"Kozen","year":"1983"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB34","first-page":"790","article-title":"Logics of programs","author":"Kozen","year":"1990"},{"issue":"6","key":"10.1016\/S0004-3702(98)00104-0_BIB35","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1093\/logcom\/1.6.761","article-title":"Compositionality through an operational semantics of contexts","volume":"1","author":"Larsen","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB36","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","article-title":"Proof systems for satisfiability in Hennessy-Milner logic with recursion","volume":"72","author":"Larsen","year":"1990","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB37","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/S0743-1066(96)00121-5","article-title":"GOLOG: A logic programming language for dynamic domains","volume":"31","author":"Levesque","year":"1997","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB38","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1016\/0004-3702(90)90021-Q","article-title":"Frames in the space of situations","volume":"46","author":"Lifschitz","year":"1990","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB39","series-title":"Proc. 4th International Conference on the Principles of Knowledge Representation and Reasoning (KR-94)","first-page":"341","article-title":"Actions with indirect effects (preliminary report)","author":"Lifshitz","year":"1994"},{"issue":"5","key":"10.1016\/S0004-3702(98)00104-0_BIB40","doi-asserted-by":"crossref","first-page":"655","DOI":"10.1093\/logcom\/4.5.655","article-title":"State constraints revisited","volume":"4","author":"Lin","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB41","series-title":"Proc. 9th National Conference on Artificial Intelligence (AAAI-91)","first-page":"349","article-title":"Provably correct theories of action (preliminary report)","author":"Lin","year":"1991"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB42","series-title":"Proc. 10th National Conference on Artificial Intelligence (AAAI-92)","first-page":"590","article-title":"Concurrent actions in the situation calculus","author":"Lin","year":"1992"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB43","series-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","first-page":"201","article-title":"The anchored version of the temporal framework","volume":"Vol. 354","author":"Manna","year":"1989"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB44","series-title":"Symbolic Model Checking","author":"McMillan","year":"1993"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB45","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB46","series-title":"Elementary Induction on Abstract Structures","author":"Moschovakis","year":"1974"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB47","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"Vol. 5","author":"Park","year":"1970"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB48","article-title":"Temporal reasoning in situation calculus","author":"Pinto","year":"1994"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB49","series-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","first-page":"359","article-title":"The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression","author":"Reiter","year":"1991"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB50","series-title":"Proc. 5th International Conference on Principles of Knowledge Representation and Reasoning (KR'96)","first-page":"2","article-title":"Natural actions, concurrency and continuous time in the situation calculus","author":"Reiter","year":"1996"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB51","series-title":"Proc. 8th International Joint Conference on Artificial Intelligence (IJCAI-81)","article-title":"Plan synthesis: A logical approach","author":"Rosenschein","year":"1981"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB52","series-title":"Proc. ICALP","first-page":"723","article-title":"Characteristic formulae","volume":"Vol. 372","author":"Steffen","year":"1989"},{"issue":"1","key":"10.1016\/S0004-3702(98)00104-0_BIB53","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1006\/inco.1994.1028","article-title":"A. Ingolfsdottir, Characteristic formulae for processes with divergence","volume":"110","author":"Steffen","year":"1994","journal-title":"Inform, and Comput."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB54","first-page":"477","article-title":"Modal and temporal logic","author":"Stirling","year":"1992"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB55","series-title":"Logics for Concurrency: Structure versus Automata","first-page":"149","article-title":"Modal and temporal logics for processes","volume":"Vol. 1043","author":"Stirling","year":"1996"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB56","series-title":"Proc. 6th International Colloquium on Automata, Languages and Programming","first-page":"465","article-title":"The propositional mu-calculus is elementary","volume":"Vol. 172","author":"Streett","year":"1984"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB57","first-page":"249","article-title":"An automata theoretic decision procedure for the propositional mu-calculus","volume":"81","author":"Streett","year":"1989","journal-title":"Inform, and Control"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB58","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB59","series-title":"Proc. ECAI'94 Workshop on Logic and Change","first-page":"153","article-title":"Interval situation calculus","author":"Ternovskaia","year":"1994"},{"issue":"5","key":"10.1016\/S0004-3702(98)00104-0_BIB60","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1093\/logcom\/4.5.811","article-title":"Modal logic, transition systems and processes","volume":"4","author":"van Benthem","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0004-3702(98)00104-0_BIB61","first-page":"278","article-title":"The linear time\u2014branching time spectrum, CONCUR'90","volume":"Vol. 458","author":"van Glabbeek","year":"1990"},{"key":"10.1016\/S0004-3702(98)00104-0_BIB62","series-title":"Proc. 11th International Colloquium on Automata, Languages and Programming","first-page":"761","article-title":"A note on model checking the modal \u03bd-calculus","volume":"Vol. 372","author":"Winskel","year":"1989"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370298001040?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370298001040?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:30:06Z","timestamp":1556411406000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370298001040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,1]]},"references-count":62,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,1]]}},"alternative-id":["S0004370298001040"],"URL":"https:\/\/doi.org\/10.1016\/s0004-3702(98)00104-0","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1999,1]]}}}