In recent years,fires in tall buildings have become more frequent,which costs billions of dollars each year and the loss of many human lives.The facade fire in the Grenfell tower made the structure uninhabitable,and t...In recent years,fires in tall buildings have become more frequent,which costs billions of dollars each year and the loss of many human lives.The facade fire in the Grenfell tower made the structure uninhabitable,and the collapse of the three World Trade Center(WTC)towers is the total structural failure caused by fire.Despite such events,no well-defined methodology exists to reconstruct both fire and structural behaviors and carrys out the forensic investigation of a building fire.This Part I paper collects the evidence of the Plasco Building fire and generates a coherent timeline to reconstruct the fire processes.The vertical and horizontal fire spread of the building is reconstructed using computational fluid dynamics(CFD)fire modeling and calibrated against the evidence library.The spatio-temporal temperature history from the fire modeling provides realistic fire scenarios to simulate the structural response.The fire simulation results are used as boundary conditions to be transferred to a finite element analysis tool for a detailed structural analysis to determine the likely collapse mechanism of the Plasco Building in Part II.The methodology presented in this paper to reconstruct the fire can also guide the structural fire safety engineers to improve the building fire-safety and life-safety strategies.展开更多
Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to...Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.展开更多
基金This research is funded by the RGC Hong Kong GRF Scheme(No.15220618)the Hong Kong Research Grants Council Theme-based Research Scheme(T22-505/19-N).
文摘In recent years,fires in tall buildings have become more frequent,which costs billions of dollars each year and the loss of many human lives.The facade fire in the Grenfell tower made the structure uninhabitable,and the collapse of the three World Trade Center(WTC)towers is the total structural failure caused by fire.Despite such events,no well-defined methodology exists to reconstruct both fire and structural behaviors and carrys out the forensic investigation of a building fire.This Part I paper collects the evidence of the Plasco Building fire and generates a coherent timeline to reconstruct the fire processes.The vertical and horizontal fire spread of the building is reconstructed using computational fluid dynamics(CFD)fire modeling and calibrated against the evidence library.The spatio-temporal temperature history from the fire modeling provides realistic fire scenarios to simulate the structural response.The fire simulation results are used as boundary conditions to be transferred to a finite element analysis tool for a detailed structural analysis to determine the likely collapse mechanism of the Plasco Building in Part II.The methodology presented in this paper to reconstruct the fire can also guide the structural fire safety engineers to improve the building fire-safety and life-safety strategies.
基金This work was supported by the French government through the UCA-Jedi project managed by the National Research Agency(ANR-15-IDEX-01)in particular,by the interdisciplinary Institute for Modeling in Neuroscience and Cognition(NeuroMod)of the UniversitéCôte d'Azur.It was also supported by the Natural Sciences and Engineering Research Council of Canada.
文摘Having a formal model of neural networks can greatly help in understanding and verifying their properties,behavior,and response to external factors such as disease and medicine.In this paper,we adopt a formal model to represent neurons,some neuronal graphs,and their composition.Some specific neuronal graphs are known for having biologically relevant structures and behaviors and we call them archetypes.These archetypes are supposed to be the basis of typical instances of neuronal information processing.In this paper we study six fundamental archetypes(simple series,series with multiple outputs,parallel composition,negative loop,inhibition of a behavior,and contralateral inhibition),and we consider two ways to couple two archetypes:(i)connecting the output(s)of the first archetype to the input(s)of the second archetype and(ii)nesting the first archetype within the second one.We report and compare two key approaches to the formal modeling and verification of the proposed neuronal archetypes and some selected couplings.The first approach exploits the synchronous programming language Lustre to encode archetypes and their couplings,and to express properties concerning their dynamic behavior.These properties are verified thanks to the use of model checkers.The second approach relies on a theorem prover,the Coq Proof Assistant,to prove dynamic properties of neurons and archetypes.