×

MILP, pseudo-Boolean, and OMT solvers for optimal fault-tolerant placements of relay nodes in mission critical wireless networks. (English) Zbl 07285109

Summary: In critical infrastructures like airports, much care has to be devoted in protecting radio communication networks from external electromagnetic interference.
Protection of such mission-critical radio communication networks is usually tackled by exploiting radiogoniometers: at least three suitably deployed radiogoniometers, and a gateway gathering information from them, permit to monitor and localise sources of electromagnetic emissions that are not supposed to be present in the monitored area. Typically, radiogoniometers are connected to the gateway through relay nodes. As a result, some degree of fault-tolerance for the network of relay nodes is essential in order to offer a reliable monitoring. On the other hand, deployment of relay nodes is typically quite expensive. As a result, we have two conflicting requirements: minimise costs while guaranteeing a given fault-tolerance.
In this paper, we address the problem of computing a deployment for relay nodes that minimises the overall cost while at the same time guaranteeing proper working of the network even when some of the relay nodes (up to a given maximum number) become faulty (fault-tolerance).
We show that, by means of a computation-intensive pre-processing on a HPC infrastructure, the above optimisation problem can be encoded as a 0/1 Linear Program, becoming suitable to be approached with standard Artificial Intelligence reasoners like MILP, PB-SAT, and SMT/OMT solvers. Our problem formulation enables us to present experimental results comparing the performance of these three solving technologies on a real case study of a relay node network deployment in areas of the Leonardo da Vinci Airport in Rome, Italy.

MSC:

68-XX Computer science
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Mancini T, Tronci E, Scialanca A, Lanciotti F, Finzi A, Guarneri R, Di Pompeo S. Optimal Fault-Tolerant Placement of Relay Nodes in a Mission Critical Wireless Network. In: Proceedings of 25th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA 2018), volume 2271 ofCEUR Workshop Proceedings. CEUR-WS.org, 2018. doi:10.29007/grw9.
[2] Alcaraz C, Zeadally S. Critical Infrastructure Protection: Requirements and Challenges for the 21st Century.International Journal of Critical Infrastructure Protection, 2015.8:53-66. doi:10.1016/j.ijcip.2014. 12.002.
[3] Skrypnik ON. Radio Navigation Systems for Airports and Airways. Springer, 2019. Q. M. Chen et al./MILP, PB & OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes255
[4] Kim Y, Kolesnikov V, Thottan M. Resilient End-to-End Message Protection for Large-Scale CyberPhysical System Communications. In: Proceedings of Third IEEE International Conference on Smart Grid Communications (SmartGridComm 2012). IEEE, 2012 pp. 193-198. doi:10.1109/SmartGridComm. 2012.6485982.
[5] Stacey D. Aeronautical Radio Communication Systems and Networks. John Wiley & Sons, 2008. ISBN 9780470018590. doi:10.1002/9780470035108.
[6] Krozel J, Andrisani D, Ayoubi M, Hoshizaki T, Schwalm C. Aircraft ADS-B Data Integrity Check. In: AIAA 4th Aviation Technology, Integration and Operations (ATIO) Forum. 2004 p. 6263.
[7] Sampigethaya K, P R. Visualization & Assessment of ADS-B Security for Green ATM. In: 29th Digital Avionics Systems Conference (DASC 2010). IEEE, 2010.
[8] McCallie D, Butts J, Mills R. Security Analysis of the ADS-B Implementation in the Next Generation Air Transportation System.International Journal of Critical Infrastructure Protection, 2011.4(2):78-87.
[9] Sch¨afer M, Lenders V, Martinovic I. Experimental Analysis of Attacks on Next Generation Air Traffic Communication. In: Proceedings of 2013 International Conference on Applied Cryptography and Network Security (ACNS 2013). Springer, 2013 pp. 253-271.
[10] Conforti M, Cornu´ejols G, Zambelli G. Integer Programming. Springer, 2014. ISBN 978-3-319-11007-3. doi:10.1007/978-3-319-11008-0.
[11] Biere A, Heule M, van Maaren H (eds.). Handbook of Satisfiability, volume 185. IOS Press, 2009. · Zbl 1183.68568
[12] Barrett C, Tinelli C. Satisfiability Modulo Theories. In: Handbook of Model Checking, pp. 305-343. Springer, 2018. doi:10.1007/978-3-319-10575-8 11. · Zbl 1392.68379
[13] Mancini T. Now or Never: Negotiating Efficiently with Unknown or Untrusted Counterparts.Fundamenta Informaticae, 2016.149(1-2):61-100. doi:10.3233/FI-2016-1443. · Zbl 1373.68412
[14] Mancini T, Mari F, Massini A, Melatti I, Tronci E. SyLVaaS: System Level Formal Verification as a Service. In: Proceedings of 23rd Euromicro International Conference on Parallel, Distributed, and NetworkBased Processing (PDP 2015). IEEE, 2015 pp. 476-483. · Zbl 1374.68294
[15] Mancini T, Mari F, Massini A, Melatti I, Merli F, Tronci E. System Level Formal Verification via Model Checking Driven Simulation. In: Proceedings of 25th International Conference on Computer Aided Verification (CAV 2013), volume 8044 ofLecture Notes in Computer Science. Springer, 2013 pp. 296-312. doi:10.1007/978-3-642-39799-8 21.
[16] Mari F, Melatti I, Salvo I, Tronci E. Synthesis of Quantized Feedback Control Software for Discrete Time Linear Hybrid Systems. In: Proceedings of 22nd International Conference on Computer Aided Verification (CAV 2010), volume 6174 ofLecture Notes in Computer Science. Springer, 2010 pp. 180- 195. doi:10.1007/978-3-642-14295-6 20. · Zbl 1362.68151
[17] Mari F, Melatti I, Salvo I, Tronci E. Model Based Synthesis of Control Software from System Level Formal Specifications.ACM Transactions on Software Engineering and Methodology, 2014.23(1):1-42. doi:10.1145/2559934.
[18] Mancini T, Mari F, Massini A, Melatti I, Tronci E. Anytime System Level Verification via Random Exhaustive Hardware In The Loop Simulation. In: Proceedings of 17th Euromicro Conference on Digital System Design (DSD 2014). IEEE, 2014 pp. 236-245.
[19] Mancini T, Mari F, Massini A, Melatti I, Tronci E. Anytime System Level Verification via Parallel Random Exhaustive Hardware in the Loop Simulation.Microprocessors and Microsystems, 2016.41:12-28. doi: 10.1016/j.micpro.2015.10.010.
[20] Mancini T, Mari F, Massini A, Melatti I, Tronci E. System Level Formal Verification via Distributed MultiCore Hardware in the Loop Simulation. In: Proceedings of 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2014). IEEE, 2014 pp. 734-742. doi:10.1109/ PDP.2014.32.
[21] Gottlob G, Greco G, Mancini T. Conditional Constraint Satisfaction: Logical Foundations and Complexity. In: Proceedings of 20th International Joint Conference on Artificial Intelligence (IJCAI 2007). 2007 pp. 88-93.
[22] Mancini T, Mari F, Melatti I, Salvo I, Tronci E, Gruber J, Hayes B, Prodanovic M, Elmegaard L. DemandAware Price Policy Synthesis and Verification Services for Smart Grids. In: Proceedings of 2014 IEEE International Conference on Smart Grid Communications (SmartGridComm 2014). IEEE, 2014 pp. 794- 799. doi:10.1109/SmartGridComm.2014.7007745.
[23] Mancini T, Mari F, Melatti I, Salvo I, Tronci E, Gruber J, Hayes B, Prodanovic M, Elmegaard L. User Flexibility Aware Price Policy Synthesis for Smart Grids. In: Proceedings of 18th Euromicro Conference on Digital System Design (DSD 2015). IEEE, 2015 pp. 478-485. doi:10.1109/DSD.2015.35.
[24] Hayes B, Melatti I, Mancini T, Prodanovic M, Tronci E. Residential Demand Management using Individualised Demand Aware Price Policies.IEEE Transactions on Smart Grid, 2017.8(3). doi: 10.1109/TSG.2016.2596790.
[25] Mancini T, Mari F, Massini A, Melatti I, Tronci E. SyLVaaS: System Level Formal Verification as a Service.Fundamenta Informaticae, 2016.1-2:101-132. doi:10.3233/FI-2016-1444. · Zbl 1374.68294
[26] Mancini T, Cadoli M. Exploiting Functional Dependencies in Declarative Problem Specifications.Artificial Intelligence, 2007.171(16-17):985-1010. · Zbl 1168.68552
[27] Mancini T, Cadoli M, Micaletto D, Patrizi F. Evaluating ASP and Commercial Solvers on the CSPLib. Constraints, 2008.13(4):407-436. doi:10.1007/s10601-007-9028-6. · Zbl 1179.90287
[28] Mancini T, Mari F, Melatti I, Salvo I, Tronci E. An Efficient Algorithm for Network Vulnerability Analysis under Malicious Attacks. In: Proceedings of The 24th International Symposium on Methodologies for Intelligent Systems (ISMIS 2018). Springer, 2018 doi:10.1007/978-3-030-01851-1 29.
[29] IBM ILOG CPLEX Optimization Studio V12.8.0, 2018. URL http://www-01.ibm.com/support/docview. wss?uid=swg27050618.
[30] GLPK (GNU Linear Programming Kit), 2012. URL http://www.gnu.org/software/glpk.
[31] Gurobi Optimizer, 2018. URL http://www.gurobi.com.
[32] E´en N, S¨orensson N. Translating Pseudo-Boolean Constraints into SAT.Journal on Satisfiability, Boolean Modeling and Computation, 2006.2:1-26. doi:10.1.1.109.4509.
[33] E´en N, S¨orensson N. An extensible SAT-solver. In: Proceedings of 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), volume 2919 ofLecture Notes in Computer Science. Springer, 2004 pp. 502-518.
[34] Pseudo-Boolean Competition 2005, 2005. URL http://www.cril.univ-artois.fr/PB05. Q. M. Chen et al./MILP, PB & OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes257
[35] Sakai M, Nabeshima H. Construction of an ROBDD for a PB-Constraint in Band form and Related Techniques for PB-solvers.IEICE Transactions on Information and Systems, 2015.E98-D, No. 6:1121- 1127.
[36] Pseudo-Boolean Competition 2016, 2016. URL http://www.cril.univ-artois.fr/PB16.
[37] Le Berre D, Parrain A. The Sat4j Library, Release 2.2.Journal on Satisfiability, Boolean Modeling and Computation, 2010.7:59-64.
[38] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), volume 4963 of Lecture Notes in Computer Science. Springer, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3 24.
[39] Bjørner N, Phan A, Fleckenstein L.νZ - An optimizing SMT solver. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015), volume 9035 ofLecture Notes in Computer Science. Springer, 2015 pp. 194-199.
[40] Sebastiani R, Trentin P. OptiMathSAT: A Tool for Optimization Modulo Theories.Journal on Satisfiability, Boolean Modeling and Computation, 2018. doi:10.1007/s10817-018-09508-6. · Zbl 1468.68206
[41] Younis M, Akkaya K. Strategies and Techniques for Node Placement in Wireless Sensor Networks: A Survey.Ad Hoc Networks, 2008.6(4):621-655. doi:10.1016/j.adhoc.2007.05.003.
[42] Hashim A, Ayinde B, Abido M. Optimal Placement of Relay Nodes in Wireless Sensor Network using Artificial Bee Colony Algorithm.Journal of Network and Computer Applications, 2016.64:239-248. doi:10.1016/j.jnca.2015.09.013.
[43] Cardei M, Du D. Improving Wireless Sensor Network Lifetime through Power Aware Organization. Wireless Networks, 2005.11(3):333-340. doi:10.1007/s11276-005-6615-6.
[44] Ganesan D, Cristescu R, Beferull-Lozano B. Power-Efficient Sensor Placement and Transmission Structure for Data Gathering under Distortion Constraints.ACM Transactions on Sensor Networks, 2006. 2(2):155-181. doi:10.1145/1149283.1149284.
[45] Amis A, Prakash R, Huynh D, Vuong T. Max-Min D-Cluster Formation in Wireless Ad Hoc Networks. In: Proceedings of 19th Annual Joint Conference of the IEEE Computer and Communications Societies (INFOCOM 2000). IEEE, 2000 pp. 32-41. doi:10.1109/INFCOM.2000.832171.
[46] Prasad R, Wu H. Gateway Deployment Optimization in Cellular Wi-Fi Mesh Networks.Journal of Networks, 2006.1(3):31-39. doi:10.4304/jnw.1.3.31-39.
[47] Biagioni E, Sasaki G. Wireless Sensor Placement For Reliable and Efficient Data Collection. In: Proceedings of 36th Hawaii International Conference on System Sciences (HICSS-36). IEEE, 2003 p. 127. doi:10.1109/HICSS.2003.1174290.
[48] Meguerdichian S, Koushanfar F, Potkonjak M, Srivastava M. Coverage Problems in Wireless Ad-hoc Sensor Networks. In: Proceedings of 20th Annual Joint Conference of the IEEE Computer and Communications Societies (INFOCOM 2001). IEEE, 2001 pp. 1380-1387. doi:10.1109/INFCOM.2001.916633.
[49] Li J, Blake C, De Couto D, Lee H, Morris R. Capacity of Ad Hoc wireless networks. In: Proceedings of 7th Annual International Conference on Mobile Computing and Networking (MOBICOM 2001). ACM. ISBN 1-58113-422-3, 2001 pp. 61-69.
[50] Krause A, Guestrin C, Gupta A, Kleinberg J. Near-Optimal Sensor Placements: Maximizing Information While Minimizing Communication Cost. In: Proceedings of 5th International Conference on Information Processing in Sensor Networks (IPSN 2006). ACM, 2006 pp. 2-10. doi:10.1145/1127777.1127782.
[51] Lee Y, Kim K, Choi Y. Optimization of AP Placement and Channel Assignment in Wireless LANs. In: Proceedings of 27th Annual IEEE Conference on Local Computer Networks (LCN 2002). IEEE, 2002 pp. 831-836. doi:10.1109/LCN.2002.1181869.
[52] Qiu L, Chandra R, Jain K, Mahdian M. Optimizing the placement of integration points in multi-hop wireless networks. In: Proceedings of 12th IEEE International Conference on Network Protocols (ICNP 2004), volume 4. IEEE, 2004 .
[53] Apt K. Principles of Constraint Programming. Cambridge University Press, 2003. · Zbl 1187.68132
[54] Rossi F, Van Beek P, Walsh T (eds.). Handbook of Constraint Programming. Elsevier, 2006. · Zbl 1175.90011
[55] Mellarkod V, Gelfond M, Zhang Y. Integrating Answer Set Programming and Constraint Logic Programming.Annals of Mathematics and Artificial Intelligence, 2008.53(1-4):251-287. · Zbl 1165.68504
[56] Lierler Y. Relating Constraint Answer Set Programming Languages and Algorithms.Artificial Intelligence, 2014.207:1-22. doi:10.1016/j.artint.2013.10.004. · Zbl 1334.68041
[57] Arias J, Carro M, Salazar E, Marple K, Gupta G. Constraint Answer Set Programming without Grounding. Theory and Practice of Logic Programming, 2018.18(3-4):337-354. · Zbl 1451.68063
[58] Hoos H, St¨utzle T. Stochastic Local Search: Foundations and Applications. Elsevier, 2004.
[59] Glover F, Kochenberger G (eds.). Handbook of Metaheuristics, volume 57. Springer, 2006.
[60] Van Hentenryck P, Michel L. Constraint-Based Local Search. MIT Press, 2009. · Zbl 1179.68141
[61] Mancini T, Flener P, Pearson J. Combinatorial Problem Solving over Relational Databases: View Synthesis through Constraint-Based Local Search. In: Proceedings of ACM Symposium on Applied Computing (SAC 2012). ACM, 2012 pp. 80-87. doi:10.1145/2245276.2245295.
[62] Tronci E, Mancini T, Salvo I, Sinisi S, Mari F, Melatti I, Massini A, Davi’ F, Dierkes T, Ehrig R, R¨oblitz S, Leeners B, Kr¨uger T, Egli M, Ille F. Patient-Specific Models from Inter-Patient Biological Models and Clinical Records. In: Proceedings of 14th International Conference on Formal Methods in ComputerAided Design (FMCAD 2014). IEEE, 2014 pp. 207-214. doi:10.1109/FMCAD.2014.6987615.
[63] Mancini T, Tronci E, Salvo I, Mari F, Massini A, Melatti I. Computing Biological Model Parameters by Parallel Statistical Model Checking. In: Proceedings of 3rd International Conference on Bioinformatics and Biomedical Engineering (IWBBIO 2015), volume 9044 ofLecture Notes in Computer Science. Springer, 2015 pp. 542-554. doi:10.1007/978-3-319-16480-9 52.
[64] Mancini T, Mari F, Massini A, Melatti I, Salvo I, Tronci E. On Minimising the Maximum Expected Verification Time.Information Processing Letters, 2017.122:8-16. doi:10.1016/j.ipl.2017.02.001. · Zbl 1422.68164
[65] Maggioli F, Mancini T, Tronci E. SBML2Modelica: Integrating Biochemical Models within OpenStandard Simulation Ecosystems.Bioinformatics, 2019. doi:10.1093/bioinformatics/btz860.
[66] Mancini T, Mari F, Massini A, Melatti I, Salvo I, Sinisi S, Tronci E, Ehrig R, R¨oblitz S, Leeners B. Computing Personalised Treatments through In Silico Clinical Trials. A Case Study on Downregulation in Assisted Reproduction. In: Proceedings of 25th RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA 2018), volume 2271 of CEUR Workshop Proceedings. CEUR-WS.org, 2018. doi:10.29007/g864.
[67] Sinisi S, Alimguzhin V, Mancini T, Tronci E, Mari F, Leeners B.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.