{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T22:00:15Z","timestamp":1766181615394},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T00:00:00Z","timestamp":1617148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T00:00:00Z","timestamp":1617148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"SINTEF AS"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper proposes a new method of combining SAT with discrete event simulation. This new integration proved useful for designing a solver for capacity analysis in early phase railway construction design. Railway capacity is complex to define and analyze, and existing tools and methods used in practice require comprehensive models of the railway network and its timetables. Design engineers working within the limited scope of construction projects report that only ad-hoc, experience-based methods of capacity analysis are available to them. Designs often have subtle capacity pitfalls which are discovered too late, only when network-wide timetables are made\u2014there is a mismatch between the scope of construction projects and the scope of capacity analysis, as currently practiced. We suggest a language for capacity specifications suited for construction projects, expressing properties such as running time, train frequency, overtaking and crossing. Such specifications can be used as contracts in the interface between construction projects and network-wide capacity analysis. We show how these properties can be verified fully automatically by building a special-purpose solver which splits the problem into two: an abstracted SAT-based dispatch planning, and a continuous-domain dynamics with timing constraints evaluated using discrete event simulation. The two components communicate in a CEGAR loop (counterexample-guided abstraction refinement). This architecture is beneficial because it clearly distinguishes the combinatorial choices on the one hand from continuous calculations on the other, so that the simulation can be extended by relevant details as needed. We describe how loops in the infrastructure can be handled to eliminate repeating dispatch plans, and use case studies based on data from existing infrastructure and ongoing construction projects to show that our method is fast enough at relevant scales to provide agile verification in a design setting. Similar SAT modulo discrete event simulation combinations could also be useful elsewhere where one or both of these methods are already applicable such as in bioinformatics or hardware\/software verification.<\/jats:p>","DOI":"10.1007\/s10703-021-00368-2","type":"journal-article","created":{"date-parts":[[2021,3,31]],"date-time":"2021-03-31T17:03:02Z","timestamp":1617210182000},"page":"211-245","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["SAT modulo discrete event simulation applied to railway design capacity analysis"],"prefix":"10.1007","volume":"57","author":[{"given":"Bj\u00f8rnar","family":"Luteberget","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Koen","family":"Claessen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Johansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,31]]},"reference":[{"key":"368_CR1","doi-asserted-by":"crossref","unstructured":"Abril, M., Barber, F., Ingolotti, L.P., Salido, M.A., Tormos, P., Lova, A.L.: An assessment of railway capacity. Transp. Res. Part E Logis. Transp. Rev. 44(5), 774\u2013806 (2008)","DOI":"10.1016\/j.tre.2007.04.001"},{"key":"368_CR2","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, IOS Press, pp. 825\u2013885 (2009)"},{"key":"368_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, Springer, pp. 305\u2013343 (2018)","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"11","key":"368_CR4","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Alessandro C, Clarke Edmund M, Ofer S, Yunshan Z et al (2003) Bounded model checking. Adv. Comput. 58(11):117\u2013148","journal-title":"Adv. Comput."},{"key":"368_CR5","doi-asserted-by":"crossref","unstructured":"Bor\u00e4lv, A., St\u00e5lmarck, G.: Formal verification in railways. In: Hinchey, M.G., Bowen, J.P. (eds.) Industrial-Strength Formal Methods in Practice, Springer, pp. 329\u2013350 (1999)","DOI":"10.1007\/978-1-4471-0523-7_15"},{"key":"368_CR6","unstructured":"Bane NOR: Model of the Norwegian rail network (2016). http:\/\/www.banenor.no\/en\/startpage1\/Market1\/Model-of-the-national-rail-network\/"},{"key":"368_CR7","doi-asserted-by":"crossref","unstructured":"Cashmore, M., Fox, M., Long, D., Magazzeni, D.: A compilation of the full PDDL+ language into SMT. In: Jane Coles, A., Coles, A., Edelkamp, S., Magazzeni, D., Sanner, S. (eds.) International Conference on Automated Planning and Scheduling, ICAPS 2016, AAAI Press, pp. 79\u201387 (2016)","DOI":"10.1609\/icaps.v26i1.13755"},{"key":"368_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV \u201900), Lecture Notes in Computer Science, vol. 1855, Springer, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"issue":"9","key":"368_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L De Moura","year":"2011","unstructured":"De Moura L, Nikolaj B (2011) Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9):69\u201377","journal-title":"Commun. ACM"},{"key":"368_CR10","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), Lecture Notes in Computer Science, vol. 4963, Springer, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"368_CR11","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) 26th Computer Aided Verification (CAC)"},{"issue":"4","key":"368_CR12","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, Niklas S (2003) Temporal induction by incremental SAT solving. Electron. Notes Theor. Comput. Sci. 89(4):543\u2013560","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"368_CR13","first-page":"308","volume":"7","author":"F Francesca","year":"2017","unstructured":"Francesca F, Roberto M, Carlo M, Paolo O, Gianpaolo O, Andrea P, Veronica P (2017) Optimal design of a regional railway service in Italy. J. Rail Transp. Plan. Manag. 7(4):308\u2013319","journal-title":"J. Rail Transp. Plan. Manag."},{"key":"368_CR14","unstructured":"Fishman, G.S.: Discrete-Event Simulation: Modeling, Programming, and Analysis. Springer Series in Operations Research, Springer (2001)"},{"key":"368_CR15","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1613\/jair.2044","volume":"27","author":"M Fox","year":"2006","unstructured":"Fox M, Derek L (2006) Modelling mixed discrete-continuous domains for planning. J Artif Intell Res 27:235\u2013297","journal-title":"J Artif Intell Res"},{"key":"368_CR16","doi-asserted-by":"publisher","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle M, Christian H, Tino T, Stefan R, Tobias S (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1:209\u2013236","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"368_CR17","unstructured":"Fujimoto RM (2000) Parallel and distributed simulation systems, Wiley"},{"key":"368_CR18","doi-asserted-by":"crossref","unstructured":"Gao S, Kong S, Clarke EM (2013) dReal: an SMT solver for nonlinear theories over the reals. In: Paola Bonacina M (ed) 24th International conference on automated deduction (CADE)","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"368_CR19","doi-asserted-by":"crossref","unstructured":"Gebser M, Janhunen T, Rintanen J (2014) SAT modulo graphs: acyclicity. InL Ferm\u00e9 E, Leite J (eds) 14th European conference on logics in artificial intelligence (JELIA)","DOI":"10.1007\/978-3-319-11558-0_10"},{"key":"368_CR20","unstructured":"Hansen IA, Pachl J (2014) Railway timetabling and operations, Eurailpress"},{"issue":"2","key":"368_CR21","first-page":"85","volume":"17","author":"S Harrod Steven","year":"2012","unstructured":"Harrod Steven S (2012) A tutorial on fundamental model structures for railway timetable optimization. Surv Oper Res Manag Sci 17(2):85\u201396","journal-title":"Surv Oper Res Manag Sci"},{"key":"368_CR22","doi-asserted-by":"crossref","unstructured":"Haxthausen AE, \u00d8stergaard PH (2016) On the use of static checking in the verification of interlocking systems. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: discussion, dissemination, applications, Springer, pp 266\u2013278","DOI":"10.1007\/978-3-319-47169-3_19"},{"key":"368_CR23","unstructured":"H\u00fcrlimann D (2002) Objektorientierte Modellierung von Infrastrukturelementen und Betriebsvorgngen im Eisenbahnwesen. PhD thesis, ETH Zurich"},{"key":"368_CR24","doi-asserted-by":"crossref","unstructured":"Isobe Y, Moller F, Nguyen HN, Roggenbach M (2012) Safety and line capacity in railways\u2014an approach in timed CSP. In: Derrick J, Gnesi S, Latella D, Treharne H (eds) 9th International conference on integrated formal methods (iFM), Lecture notes in computer science, Springer, pp 54\u201368","DOI":"10.1007\/978-3-642-30729-4_5"},{"issue":"3\/4","key":"368_CR25","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovic","year":"2012","unstructured":"Jovanovic D, de Moura L (2012) Solving non-linear arithmetic. ACM Commun Comput Algebra 46(3\/4):104\u2013105","journal-title":"ACM Commun Comput Algebra"},{"key":"368_CR26","doi-asserted-by":"crossref","unstructured":"Kamburjan E, H\u00e4hnle R (2016) Uniform modeling of railway operations. In: Formal techniques for safety-critical systems FTSCS 2016, Communications in computer and information science, vol 694, Springer, pp 55\u201371","DOI":"10.1007\/978-3-319-53946-1_4"},{"issue":"1","key":"368_CR27","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1287\/opre.2014.1327","volume":"63","author":"L Leonardo","year":"2015","unstructured":"Leonardo L, Carlo M (2015) An exact decomposition approach for the real-time train dispatching problem. Oper Res 63(1):48\u201364","journal-title":"Oper Res"},{"key":"368_CR28","unstructured":"Landex A (2008) Methods to estimate railway capacity and passenger delays. PhD thesis, Technical University of Denmark (DTU)"},{"issue":"1\u20132","key":"368_CR29","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/j.artint.2004.04.004","volume":"157","author":"F Lin","year":"2004","unstructured":"Lin F, Yuting Z (2004) ASSAT: computing answer sets of a logic program by SAT solvers. Artif Intell 157(1\u20132):115\u2013137","journal-title":"Artif Intell"},{"key":"368_CR30","unstructured":"LUKS: Analysis of lines and junctions. Software web page: http:\/\/www.via-con.de\/development\/luks (2018)"},{"key":"368_CR31","doi-asserted-by":"crossref","unstructured":"Luteberget B, Camilleri JJ, Johansen C, Schneider G (2017) Participatory verification of railway infrastructure by representing regulations in RailCNL. In: Cimatti A, Sirjani L (eds) International conference on software engineering and formal methods (SEFM)","DOI":"10.1007\/978-3-319-66197-1_6"},{"key":"368_CR32","doi-asserted-by":"crossref","unstructured":"Luteberget B, Claessen K, Johansen C (2018) Design-time railway capacity verification using SAT modulo discrete event simulation. In: Bj\u00f8rner N, Gurfinkel A (eds) Formal methods in computer aided design (FMCAD), IEEE, pp 1\u20139","DOI":"10.23919\/FMCAD.2018.8603003"},{"issue":"1","key":"368_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-017-0281-z","volume":"52","author":"B Luteberget,","year":"2018","unstructured":"Luteberget, B, Christian J (2018) Efficient verification of railway infrastructure designs against standard regulations. Formal Methods Syst. Des. 52(1):1\u201332","journal-title":"Formal Methods Syst. Des."},{"key":"#cr-split#-368_CR34.1","doi-asserted-by":"crossref","unstructured":"Luteberget B, Johansen C, Steffen M (2016) Rule-based consistency checking of railway infrastructure designs. In: \u00c1brah\u00e1m E, Huisman M","DOI":"10.1007\/978-3-319-33693-0_31"},{"key":"#cr-split#-368_CR34.2","unstructured":"(ed) Integrated formal methods 2016, Lecture notes in computer science, vol 9681, Springer, pp 491-507"},{"key":"368_CR35","unstructured":"Montigel M (1994) Modellierung und Gew\u00e4hrleistung von Abh\u00e4ngigkeiten in Eisenbahnsicherungsanlagen. PhD thesis, ETH Zurich"},{"key":"368_CR36","unstructured":"Nash A, Huerlimann D, Sch\u00fctte J, Krauss VP (2004) RailML\u2014a standard data interface for railroad applications. In: Computers in railways, vol IX, WIT Press, pp 233\u2013240"},{"issue":"6","key":"368_CR37","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Albert O, Cesare T (2006) Solving SAT and SAT modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"368_CR38","unstructured":"OpenTrack: Simulation of railway networks. Software web page: http:\/\/www.opentrack.ch\/ (2018)"},{"key":"368_CR39","unstructured":"Pachl J (2015) Railway operation and control. VTD Rail Publishing"},{"key":"#cr-split#-368_CR40.1","doi-asserted-by":"crossref","unstructured":"Piotrowski WM, Fox M, Long D, Magazzeni D, Mercorio F (2016) Heuristic planning for PDDL+ domains. In: Kambhampati S","DOI":"10.1609\/aaai.v30i1.9953"},{"key":"#cr-split#-368_CR40.2","unstructured":"(ed) International joint conference on artificial intelligence, IJCAI 2016, IJCAI\/AAAI Press, pp 3213-3219"},{"key":"368_CR41","unstructured":"railML (2018) The XML interface for railway applications. Organization web page: http:\/\/www.railml.org"},{"key":"368_CR42","volume-title":"Simulation: the practice of model development and use","author":"R Stewart","year":"2004","unstructured":"Stewart R (2004) Simulation: the practice of model development and use. Wiley, New York"},{"issue":"3\u20134","key":"368_CR43","first-page":"141","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani R (2007) Lazy satisability modulo theories. J Satis Boolean Model Comput 3(3\u20134):141\u2013224","journal-title":"J Satis Boolean Model Comput"},{"key":"368_CR44","doi-asserted-by":"crossref","unstructured":"Sinz C (2005) Towards an optimal CNF encoding of Boolean cardinality constraints. In: van Beek P (ed) Principles and practice of constraint programming. Lecture notes in computer science, vol 3709, Springer, pp 827\u2013831","DOI":"10.1007\/11564751_73"},{"key":"368_CR45","unstructured":"Vu LH, Haxthausen AE, Peleska J (2014) A domain-specific language for railway interlocking systems. In: 10th Symposium on formal methods for automation and safety in railway and automotive systems, TU Braunschweig, pp 200\u2013209"},{"issue":"1","key":"368_CR46","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/S0377-2217(00)00087-4","volume":"128","author":"PJ Zwaneveld","year":"2001","unstructured":"Zwaneveld PJ, Kroon LG, van Hoesel SPM (2001) Routing trains through a railway station based on a node packing model. Eur J Oper Res 128(1):14\u201333","journal-title":"Eur J Oper Res"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00368-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00368-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00368-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,23]],"date-time":"2022-12-23T01:35:03Z","timestamp":1671759303000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00368-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,31]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["368"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00368-2","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3,31]]},"assertion":[{"value":"19 March 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 March 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}