MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks

• Autorzy: Chen Qian Matteo , Finzi Alberto , Mancini Toni , Melatti Igor , Tronci Enrico

Identyfikatory

DOI

10.3233/FI-2020-1941

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

telecommunication systems; radio; satisfiability; computer science; radio networks; electromagnetic interference; artificial intelligence

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 174, nr 3/4
• Strony: 229--258
• Opis fizyczny: Bibliogr. 67 poz., rys., tab., wykr.

Twórcy

autor

Chen Qian Matteo

• Computer Science Department, Sapienza University of Rome, Italy

autor

Finzi Alberto

• Department of Electrical Engineering and Information Technology, University of Naples Federico II, Italy

autor

Mancini Toni

• Computer Science Department, Sapienza University of Rome, Italy

autor

Melatti Igor

• Computer Science Department, Sapienza University of Rome, Italy

autor

Tronci Enrico

• Computer Science Department, Sapienza University of Rome, Italy

Bibliografia

• [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 of CEUR 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.
• [4] Kim Y, Kolesnikov V, Thottan M. Resilient End-to-End Message Protection for Large-Scale Cyber-Physical 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äfer 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éjols 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.
• [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.
• [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.
• [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 Network-Based Processing (PDP 2015). IEEE, 2015 pp. 476-483.
• [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 of Lecture 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 of Lecture Notes in Computer Science. Springer, 2010 pp. 180-195. doi:10.1007/978-3-642-14295-6_20.
• [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 Multi-Core 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. Demand-Aware 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.
• [26] Mancini T, Cadoli M. Exploiting Functional Dependencies in Declarative Problem Specifications. Artificial Intelligence, 2007. 171(16-17):985-1010.
• [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.
• [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én N, Sörensson 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én N, Sörensson N. An extensible SAT-solver. In: Proceedings of 6th International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), volume 2919 of Lecture Notes in Computer Science. Springer, 2004 pp. 502-518.
• [34] Pseudo-Boolean Competition 2005, 2005. URL http://www.cril.univ-artois.fr/PB05.
• [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. vZ - 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 of Lecture 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.
• [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.
• [54] Rossi F, Van Beek P, Walsh T (eds.). Handbook of Constraint Programming. Elsevier, 2006.
• [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.
• [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.
• [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.
• [58] Hoos H, Stützle 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.
• [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öblitz S, Leeners B, Krüger 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 Computer-Aided 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 of Lecture 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.
• [65] Maggioli F, Mancini T, Tronci E. SBML2Modelica: Integrating Biochemical Models within Open-Standard 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öblitz 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. Optimal Personalised Treatment Computation through In Silico Clinical Trials on Patient Digital Twins. Fundamenta Informaticae, 2020. To appear.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).