{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T14:29:43Z","timestamp":1784644183573,"version":"3.55.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,7,22]],"date-time":"2017-07-22T00:00:00Z","timestamp":1500681600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,7,22]],"date-time":"2017-07-22T00:00:00Z","timestamp":1500681600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1138860"],"award-info":[{"award-number":["CCF-1138860"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1139138"],"award-info":[{"award-number":["CCF-1139138"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1421122"],"award-info":[{"award-number":["CNS-1421122"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1007\/s10817-017-9420-x","type":"journal-article","created":{"date-parts":[[2017,7,22]],"date-time":"2017-07-22T16:17:45Z","timestamp":1500740265000},"page":"107-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":51,"title":["Synthesis of Obfuscation Policies to Ensure Privacy and Utility"],"prefix":"10.1007","volume":"60","author":[{"given":"Yi-Chin","family":"Wu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Vasumathi","family":"Raman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Blake C.","family":"Rawlings","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"St\u00e9phane","family":"Lafortune","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,7,22]]},"reference":[{"issue":"4","key":"9420_CR1","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/s10626-007-0020-5","volume":"17","author":"E Badouel","year":"2007","unstructured":"Badouel, E., Bednarczyk, M., Borzyszkowski, A., Caillaud, B., Darondeau, P.: Concurrent secrets. Discrete Event Dyn. Syst. 17(4), 425\u2013446 (2007). doi:\n                    10.1007\/s10626-007-0020-5","journal-title":"Discrete Event Dyn. Syst."},{"issue":"8","key":"9420_CR2","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"9420_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"9420_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"CG Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer, Berlin (2008). doi:\n                    10.1007\/978-0-387-68612-7"},{"key":"9420_CR5","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Computer Aided Verification, Lecture Notes in Computer Science, pp. 359\u2013364. doi:\n                    10.1007\/3-540-45657-0_29\n                    \n                   (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"2","key":"9420_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. Assoc. Comput. Mach. Trans. Program. Lang. Syst. 8(2), 244\u2013263 (1986). doi:\n                    10.1145\/5397.5399","journal-title":"Assoc. Comput. Mach. Trans. Program. Lang. Syst."},{"issue":"5","key":"9420_CR7","doi-asserted-by":"publisher","first-page":"1089","DOI":"10.1109\/TAC.2010.2042008","volume":"55","author":"J Dubreil","year":"2010","unstructured":"Dubreil, J., Darondeau, P., Marchand, H.: Supervisory control for opacity. IEEE Trans. Autom. Control 55(5), 1089\u20131100 (2010). doi:\n                    10.1109\/tac.2010.2042008","journal-title":"IEEE Trans. Autom. Control"},{"key":"9420_CR8","doi-asserted-by":"crossref","unstructured":"Dwork, C.: Differential privacy. In: International Conference on Automata, Languages and Programming, pp. 1\u201312 (2006)","DOI":"10.1007\/11787006_1"},{"key":"9420_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-015-0223-0","author":"R Ehlers","year":"2016","unstructured":"Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.Y.: Supervisory control and reactive synthesis: a comparative introduction. Discrete Event Dyn. Syst. (2016). doi:\n                    10.1007\/s10626-015-0223-0","journal-title":"Discrete Event Dyn. Syst."},{"key":"9420_CR10","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1090\/dimacs\/031\/06","volume":"31","author":"EA Emerson","year":"1997","unstructured":"Emerson, E.A.: Model checking and the mu-calculus. DIMACS Ser. Discrete Math. 31, 185\u2013214 (1997)","journal-title":"DIMACS Ser. Discrete Math."},{"key":"9420_CR11","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Marchand, H.: Runtime enforcement of K-step opacity. In: 52nd IEEE Conference on Decision and Control (2013)","DOI":"10.1109\/CDC.2013.6761043"},{"key":"9420_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science. Cambridge University Press, Cambridge (2004). doi:\n                    10.1017\/cbo9780511810275"},{"key":"9420_CR13","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/j.arcontrol.2016.04.015","volume":"41","author":"R Jacob","year":"2016","unstructured":"Jacob, R., Lesage, J.J., Faure, J.M.: Overview of discrete event systems opacity: models, validation, and quantification. Annu. Rev. Control 41, 135\u2013146 (2016). doi:\n                    10.1016\/j.arcontrol.2016.04.015","journal-title":"Annu. Rev. Control"},{"issue":"3","key":"9420_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"9420_CR15","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-642-17511-4_28","volume":"6355","author":"O Kupferman","year":"2010","unstructured":"Kupferman, O., Tamir, T.: Coping with selfish on-going behaviors. Log. Program. Artif. Intell. Reason. 6355, 501\u2013516 (2010)","journal-title":"Log. Program. Artif. Intell. Reason."},{"issue":"1\u20132","key":"9420_CR16","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/s10207-004-0046-8","volume":"4","author":"J Ligatti","year":"2005","unstructured":"Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1\u20132), 2\u201316 (2005). doi:\n                    10.1007\/s10207-004-0046-8","journal-title":"Int. J. Inf. Secur."},{"key":"9420_CR17","doi-asserted-by":"crossref","unstructured":"O\u2019Kane, J.M., Shell, D.A.: Automatic design of discreet discrete filters. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 353\u2013360 (2015)","DOI":"10.1109\/ICRA.2015.7139023"},{"issue":"1","key":"9420_CR18","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"PJ Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"key":"9420_CR19","unstructured":"Rawlings, B.C.: Discrete dynamics in chemical process control and automation. Ph.D. thesis, Carnegie Mellon University (2016)"},{"key":"9420_CR20","doi-asserted-by":"publisher","unstructured":"Rawlings, B.C., Christenson, B., Wassick, J., Ydstie, B.E.: Supervisor synthesis to satisfy safety and reachability requirements in chemical process control. In: 12th International Workshop on Discrete Event Systems, pp. 195\u2013200, (2014). doi:\n                    10.3182\/20140514-3-FR-4046.00127","DOI":"10.3182\/20140514-3-FR-4046.00127"},{"issue":"5","key":"9420_CR21","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1109\/TAC.2011.2170453","volume":"57","author":"A Saboori","year":"2012","unstructured":"Saboori, A., Hadjicostis, C.N.: Opacity-enforcing supervisory strategies via state estimator constructions. IEEE Trans. Autom. Control 57(5), 1155\u20131165 (2012)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"9420_CR22","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000). doi:\n                    10.1145\/353323.353382","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"9420_CR23","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 2.3.0. University of Colorado at Boulder (1998)"},{"issue":"5","key":"9420_CR24","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1016\/j.automatica.2014.02.038","volume":"50","author":"YC Wu","year":"2014","unstructured":"Wu, Y.C., Lafortune, S.: Synthesis of insertion functions for enforcement of opacity security properties. Automatica 50(5), 1336\u20131348 (2014)","journal-title":"Automatica"},{"key":"9420_CR25","doi-asserted-by":"publisher","unstructured":"Wu, Y.C., Raman, V., Lafortune, S., Seshia, S.A.: Obfuscator synthesis for privacy and utility. In: NASA Formal Methods, Lecture Notes in Computer Science, pp. 133\u2013149, (2016). doi:\n                    10.1007\/978-3-319-40648-0_11","DOI":"10.1007\/978-3-319-40648-0_11"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9420-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9420-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9420-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T22:59:52Z","timestamp":1589410792000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9420-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,22]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["9420"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9420-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,22]]},"assertion":[{"value":"5 December 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 July 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 July 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}